GADTs/existentials can hide values with custom type errors
Summary
In GADTs, you can construct nested values where the inner values should not be constructable due to custom type errors.
Steps to reproduce
We can define a type family containing a type error:
type family OhNo where
OhNo = TypeError (Text "Oh no")
We can define a GADT parametrised by this type error:
data Bar (k :: b) where
Bar :: Bar OhNo
deriving instance Show (Bar k)
We get an error that no value Bar
can be constructed due to the error:
*Main> Bar
<interactive>:23:1: error:
• Oh no
• When checking the inferred type
it :: forall b. Bar (TypeError ...)
But we can hide the type error as an existential:
data SomeBar where
SomeBar :: Bar k -> SomeBar
deriving instance Show SomeBar
*Main> SomeBar Bar
SomeBar Bar
Expected behavior
I would have expected the expression SomeBar Bar
not to be well-typed. The custom type error should have been triggered.
Environment
- GHC version used: 8.10.4