Untouchable variable in unused let binding

Summary

When using GADTs, we observed a surprising "untouchable type variable" error on innocuous-seeming code involving pattern matching on the GADT's sole constructor in a let binding. It may be that everything is operating as designed, but the scenario seemed fragile enough and surprising enough to warrant a report.

Steps to reproduce

The following code exhibits the issue:

{-# language GADTs #-}
module Untouchable where

data T a where
    MkT :: Bool -> T Bool

fine :: T a -> Int
fine x = let MkT y = x in if y then 1 else 2

sure :: T Bool -> Int
sure x = let MkT y = x in 3

nope :: T a -> Int
nope x = let MkT y = x in 3

fine and sure compile with no issues, but nope causes an error:

    • Couldn't match expected type ‘p0’ with actual type ‘Bool’
        ‘p0’ is untouchable
          inside the constraints: a ~ Bool
          bound by a pattern with constructor: MkT :: Bool -> T Bool,
                   in a pattern binding
          at src/Main.hs:14:14-18
    • In the pattern: MkT y
      In a pattern binding: MkT y = x
      In the expression: let MkT y = x in 3

Expected behavior

We expected that either nope would compile, or else sure would fail to compile.

Environment

• GHC version used: 8.8.3, 8.6.5