Partial type signature variable confuses instance solving
When I say
{-# LANGUAGE TypeFamilies, GADTs #-}
module Bug where
f :: (a ~ [b]) => T a -> _ -> String
f (MkT x) _ = show x
data T a where
MkT :: G a => a -> T a
type family G a where
G [b] = Show b
I get
Bug.hs:6:1: error:
• Could not deduce (Show b)
from the context: a ~ [b]
bound by the inferred type for ‘f’:
forall a b {w}. (a ~ [b]) => T a -> w -> String
at Bug.hs:6:1-20
• When checking that the inferred type
f :: forall {a} {b} {w}. (a ~ [b], Show [b]) => T a -> w -> String
is as general as its (partial) signature
f :: forall a b {w}. (a ~ [b]) => T a -> w -> String
We end up with
[G] Show b[tyv:1]
[W] Show [b[tyv:1]]
The check in matchableGivens
considers b
a meta-variable. This isn't entirely wrong, but b
is a TyVarTv
, and should not be considered unifiable in matchableGivens
. The solution is very easy: just change matchableGivens
to treat TyVarTv
s like skolems.