GHC.TypeLits.TypeError can print 'GHC.Types.Any' when existentials are involved
I've run into a situation where GHC seems to forget some information.
Specifically: when wrapping type-level information into a promoted existential datatype, and then unwrapping it, Any
can appear.
I've boiled it down to the following simple example:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module AnyTypeError where
import GHC.TypeLits
( TypeError, ErrorMessage(..) )
data A = MkA
data B (a :: A)
data TySing ty where
SB :: TySing (B a)
data ATySing where
MkATySing :: TySing ty -> ATySing
type family Forget ty :: ATySing where
Forget (B a) = MkATySing SB
type family Message ty where
Message (MkATySing (_ :: TySing ty)) =
TypeError ( ShowType ty )
type KnownType = B MkA
foo :: Message (Forget KnownType) => ()
foo = ()
bar :: ()
bar = foo
AnyTypeError.hs:36:7: error:
* B GHC.Types.Any
* In the expression: foo
In an equation for `bar': bar = foo
|
36 | bar = foo
| ^^^
Failed, no modules loaded.
I think the error message should instead be:
AnyTypeError.hs:36:7: error:
* B 'MkA
...
I ran into this code when working on giving helpful custom type errors. In a library I'm working on, the user can layout vertex data passed to the GPU by specifing interface slots (see e.g. the OpenGL wiki for reference). For instance the following would be an invalid layout: After some lengthy type-level computations with type families (involving existential types similar to those described above), I need to throw an error: the The size of the vectors are lost, so the error message becomes confusingly vague. Show/hide background information (i.e. why this matters to me).
type InvalidLayout = '[ Slot 0 0 ':-> V 3 Double, Slot 1 0 ':-> V 4 Float ]
V 4 Double
spills into the second slot (Slot 1
) so overlaps with the V 4 Float
. However the error message I end up throwing, because of the bug described here, comes out looking like this: * Overlap at location 1, component 0:
- V GHC.Types.Any Double based at location 0, component 0,
- V GHC.Types.Any Float based at location 1, component 0.
I've tested this on GHC 8.6.5, 8.8.1 and HEAD (8.9.0.20190930), all giving identical results.