/home/sandy/Vik.hs:11:20: error:
• Couldn't match expected type ‘b’ with actual type ‘b1’
‘b1’ is a rigid type variable bound by
a pattern with constructor:
Temp :: forall a b. Model a b => b -> Temp a,
in an equation for ‘getTemp’
at /home/sandy/Vik.hs:11:10-15
‘b’ is a rigid type variable bound by
the type signature for:
getTemp :: forall a b. Model a b => Temp a -> b
at /home/sandy/Vik.hs:10:1-35
• In the expression: a
In an equation for ‘getTemp’: getTemp (Temp a) = a
• Relevant bindings include
a :: b1 (bound at /home/sandy/Vik.hs:11:15)
getTemp :: Temp a -> b (bound at /home/sandy/Vik.hs:11:1)
|
11 | getTemp (Temp a) = a
|
more generally the problem i'm trying to solve is that given some opaque datatype A that i can define arbitrarily to my liking, and an instance Model A B, i want to write a bunch of code that uses B but refers to A in the type signature
@Sandy Maguire That isn’t a bug in GHC, it’s the way fundeps are designed (for better or for worse). Fundeps don’t provide evidence the way type equalities against type families do, they just affect type inference.
What does that mean in practice? It means that if you have
classCab|a->binstanceCIntBool
and you end up with a C Int a given, you cannot deduce a a ~ Bool given! Instead, all the fundep does is cause a new a ~ Boolwanted to be emitted. If a is a solver variable, this makes nice things happen: a will be solved to Bool, and you get nice type inference. But if a is rigid, you get nothing: you just end up with an a ~ Bool wanted that you cannot solve.
You have to think of fundeps as “inference guides,” not sources of evidence. (The formal term for this “inference guiding” is “improvement,” introduced by Mark P. Jones in his work on qualified types.) Unless something fundamental changes in GHC’s treatment of functional dependencies, you will never be able to acquire type equality evidence from a functional dependency alone, since it simply doesn’t exist.
I would expect this to work, but it doesn't.
shouldn't the fundep here be enough to unify
b ~ b1
?given that
model
is library code i want to interface with, how can i do this?more generally the problem i'm trying to solve is that given some opaque datatype
A
that i can define arbitrarily to my liking, and an instanceModel A B
, i want to write a bunch of code that usesB
but refers toA
in the type signaturebut sandy! you must be mad!
getTemp (Temp a) = a
is pretty confusing, tripped me up for a minute. It's probably easier to read if you replaced the as with bs :DBut I would have also expected that to work
i want to write code of the form:
and then invoke it with something like
f (unmodel $ something of type B)
such that the definition of
A
andunmodel
are entirely mechanical and require no thought from me whatsoever as the user of this libraryModel
is library code is what makes this particularly hard I thinkBecause trying out stuff like making it an associated type rather than fundep is out of the question (not even sure if it would fix the problem)
yeah
i think this is a bug in ghc
i don't think it can be a tyfam because the injectivity goes the wrong way
nevermind; the injectivity annotation isn't necessary in the tyfam
that one would work
(and does)
datatype context doesn't work due to NOT WORKING ON GADTs
oh i wonder if i can do a dumb trick
this doesnt work :(
@Sandy Maguire That isn’t a bug in GHC, it’s the way fundeps are designed (for better or for worse). Fundeps don’t provide evidence the way type equalities against type families do, they just affect type inference.
What does that mean in practice? It means that if you have
and you end up with a
C Int a
given, you cannot deduce aa ~ Bool
given! Instead, all the fundep does is cause a newa ~ Bool
wanted to be emitted. Ifa
is a solver variable, this makes nice things happen:a
will be solved toBool
, and you get nice type inference. But ifa
is rigid, you get nothing: you just end up with ana ~ Bool
wanted that you cannot solve.You can see this for yourself by writing the following very simple program:
This program will not compile.
You have to think of fundeps as “inference guides,” not sources of evidence. (The formal term for this “inference guiding” is “improvement,” introduced by Mark P. Jones in his work on qualified types.) Unless something fundamental changes in GHC’s treatment of functional dependencies, you will never be able to acquire type equality evidence from a functional dependency alone, since it simply doesn’t exist.
The type family equivalent works because you explicitly pass around evidence for a type equality. If you write
then when you write
foo
, it typechecks because you can get thea ~ B Int
evidence out of theC2
dictionary’s superclass dictionaries.(It can be helpful to think of
a ~ b
constraints as implicitly-passeda :~: b
values, since in GHC, that’s exactly what they are.)that's helpful, thanks @Alexis King .
apparently i've been away from Hs too long! I didn't even think about passing around
:~:
smaybe it's just because it's early and i'm still in bed, but i don't see how to make this work with explicit Refls either
i came up with a boring solution :)