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]
