GitLab

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 TyVarTvs like skolems.