GADT pattern match defeats instance solving
When I say
{-# LANGUAGE GADTs #-}
-- NB: NO FlexibleContexts
module Bug where
data T a where
MkT :: Show a => [a] -> T a
f (MkT x) = show x
GHC says
Bug.hs:8:1: error:
• Non type-variable argument in the constraint: Show [a]
(Use FlexibleContexts to permit this)
• When checking the inferred type
f :: forall {a}. Show [a] => T a -> String
The problem is that GHC wants to infer f :: Show [a] => T a -> String
. Yet the correct type is f :: Show a => T a -> String
, with the simplified Show a
constraint.
The reason this happens is that the solver ends up in this scenario:
at level 2
[G] Show alpha[tau:1]
[W] Show [alpha[tau:1]]
Before committing to the top-level Show a => Show [a]
instance, GHC checks whether any Givens might fire later. It worries Show alpha
might apply later. But this would be impossible unless alpha
becomes an infinitely nested list. There is already logic in lookupInstEnv'
to usefully ignore such absurdities in instance lookup (see Note [Infinitary substitution in lookup]
in GHC.Core.InstEnv), and we should extend this logic to matchableGivens
.