GitLab

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
    ...

Show/hide background information (i.e. why this matters to me).

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:

type InvalidLayout = '[ Slot 0 0 ':-> V 3 Double, Slot 1 0 ':-> V 4 Float ]

After some lengthy type-level computations with type families (involving existential types similar to those described above), I need to throw an error: the 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.

The size of the vectors are lost, so the error message becomes confusingly vague.

I've tested this on GHC 8.6.5, 8.8.1 and HEAD (8.9.0.20190930), all giving identical results.