Approximately, what is happening here is this: in order to discover that
your '_' should be 'a -> a', GHC first makes '_' a unification variable
('w'), later discovers that w must equal a -> a, and then finally
crystallises (zonks) types to make the _ equal to a -> a.
This process is standard Hindley-Milner, and remember that the goal of
Hindley-Milner is to derive a "principal type": _the_ most general type
that fits in a particular place.
Once you add equality constraints to a context, however, this standard
H-M procedure does not necessarily lead to the most general type any
more. Suppose you write a function as follows:
foo :: Proxy a -> Proxy b -> a :~: b -> _
foo (Proxy @a) _ Refl = (id :: a -> a)
What should GHC put on the '_'? a -> a, or b -> b, or a -> b, or b -> a?
All are valid, because under the a ~ b equality brought in scope by the
Refl, all are equal. There is no single most general type, and note that
these types are in fact all distinct because the (:~:) value may be
undefined, and 'a' might actually be unequal to 'b'.
As a result, GHC is very cautious when it has a unification variable
created _outside_ the scope of a particular equality constraint and gets
evidence for the value of that variable _inside_ that constraint. Such
unification variables are called "rigid" -- this is why this term occurs
in your type error. This sometimes results in GHC being seemingly
over-cautious, like in your case -- but note that `fromDict :: Dict (C
a) -> T a -> T a` is also type-correct!
Type inference is only all-powerful as long as you remain in the
Hindley-Milner fragment of the language, and equality constraints are
not in that fragment. Hence you need more type signatures.
- Tom
On 13/11/2025 14:09, Wolfgang Jeltsch wrote:
Hi!
Some code of mine doesn’t pass the type checker, and I have no clue to
what problem GHC’s error message is meant to point.
Consider the following reduced variant of my code:
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeAbstractions #-}
{-# LANGUAGE PartialTypeSignatures #-}
data Dict c = c => Dict
class T a ~ a => C a where
type T a :: *
op :: C a => a -> a
op = undefined
fromDict :: Dict (C a) -> _
fromDict (Dict @(C a)) = op @a
Feeding this to GHC 9.12.2 results in GHC telling me that it “could not
deduce `w ~ (a -> a)` from the context `C a`” bound by the argument
pattern of `fromDict`, where “`w` is a rigid type variable bound by the
inferred type of `fromDict`”, which is “`Dict (C a) -> w`” and that this
all happened “in the expression `op @a`”.
After removing the constraint `T a ~ a` from the class declaration, the
code is accepted.
At the moment, I don’t understand at all why the presence of an equality
constraint should make this program type-incorrect, and I also don’t
understand the error message, in particular the role of that rigid type
variable `w`.
Could someone perhaps enlighten me? 🙂
All the best,
Wolfgang
_______________________________________________
ghc-devs mailing list -- [email protected]
To unsubscribe send an email to [email protected]
_______________________________________________
ghc-devs mailing list -- [email protected]
To unsubscribe send an email to [email protected]
