Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.
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)
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
case singFor of
STrue -> False
SFalse -> True
f and g don't compile (guessing here):
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.
I don't think you can get around this without any sort of plugin
Feels like it.
I wonder if there is something inconsistent about making this the default behaviour
It would introduce ambiguity in cases where there are multiple valid instances of same type in scope
what do you expect this program to do?
> g @True
> f @True
i.e. propagate the initial type argument silently
ah i see
it's arguably a failing of hs
YouTube - YOW! Lambda Jam 2016 Conor McBride - What are Types for, or are they only Against? #YOWLambdaJam talks about this if you are interested
or more specifically, why things are this way
the early FP people wanted to infer all of their types! ALL Of THEM
even top level things
and so a lot of the language's early design implicit comes with the assumption that types should be invisible
hopefully we can move to something more liberal
I guess I'll go looking on ghcs issues/proposals