Automatic propagation of "unused" constraints

2020-05-03 14:00:19

Is it possible to automatically propagate type class constraints which have no arguments associated with them? (when there is only one eligible constraint in scope)
Example:

{-# LANGUAGE
   DataKinds,
   GADTs,
   KindSignatures,
   AllowAmbiguousTypes #-}

import Data.Kind (Type)

data SBool (b :: Bool) where
  SFalse :: SBool 'False
  STrue :: SBool 'True

class HasSing (b :: Bool) where
  singFor :: SBool b

instance HasSing 'True where
  singFor = STrue

instance HasSing 'False where
  singFor = SFalse

f :: HasSing b => Bool
f = not $ g

g :: HasSing b => Bool
g =
  case singFor of
    STrue -> False
    SFalse -> True

f and g don't compile (guessing here):

in f the g call doesn't infer that the available HasSing b is to be used
in g the singFor call doesn't infer that the available HasSing b is to be used

If I use ScopedTypeVariables and TypeApplications I can work around this, but it goes against my original goal of implicitly passing around a singleton, as now I have to write type applications wherever I would previously pass a singleton explicitly.
There is also a situation in which I don't know how to refer to the type argument as of current ghc - case matching on gadt constructors which have forall'd types in them.
Can I work around this somehow, while keeping automatic propagation in non-ambiguous uses (only one constraint in scope)?

I looked at reflection and it also has this issue (when using Given+given at least).
polysemy solves this issue via polysemy-plugin.