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 -- ghc-devs@haskell.org To unsubscribe send an email to ghc-devs-leave@haskell.org