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