Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
  • GHC GHC
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 5,243
    • Issues 5,243
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 570
    • Merge requests 570
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
    • Test Cases
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Code review
    • Insights
    • Issue
    • Repository
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Glasgow Haskell CompilerGlasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #17301
Closed
Open
Issue created Oct 04, 2019 by sheaf@sheafMaintainer

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

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.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking