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