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.