Opened 9 months ago

Last modified 9 months ago

#14514 new bug

Error messages: suggest annotating with higher-rank kind

Reported by: Iceland_jack Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.2.1
Keywords: TypeInType, TypeErrorMessages Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by goldfire)

The ticket below was posted because of confusion around higher-rank kinds. comment:3 suggests an error-message improvement, which I (goldfire) think is feasible.


Following code from Richard's 2016 Haskell Implementors' Workshop talk (/ Trees That Grow) works just fine

{-# Language RankNTypes, KindSignatures, DataKinds, TypeFamilyDependencies, TypeInType #-}

import Data.Kind

data TagTag = ETagTag | PTagTag
data ETag   = VarTag
data PTag   = VarPTag

type family
  Tag (ttag::TagTag) = (res :: Type) | res -> ttag where
  Tag ETagTag = ETag
  Tag PTagTag = PTag

type WithAnyTag = forall tag. Tag tag -> Type

-- data Exp (ext::WithAnyTag) where
--   Var :: ext VarTag -> Exp ext
data Exp (ext::WithAnyTag) = Var (ext VarTag)

but replace data Exp with its commented-out GADT brethren and it stops working

$ ghci -ignore-dot-ghci Weird.hs 
GHCi, version 8.2.1: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( Weird.hs, interpreted )

Weird.hs:17:28: error:
    • Expected kind ‘WithAnyTag’, but ‘ext1’ has kind ‘ETag -> *’
    • In the first argument of ‘Exp’, namely ‘ext’
      In the type ‘Exp ext’
      In the definition of data constructor ‘Var’
   |
17 |   Var :: ext VarTag -> Exp ext
   |                            ^^^
Failed, 0 modules loaded.
Prelude> 

The type synonym can be inlined, makes no difference.

Change History (5)

comment:1 Changed 9 months ago by Iceland_jack

I suppose the answer is that “GHC never infers a higher-rank kind”.

The correct way of writing this is explicitly quantifying over the kind of ext when writing it as a GADT (as is done here: TypeRepX)

data Exp :: WithAnyTag -> Type where
  Var :: forall (ext::WithAnyTag). ext VarTag -> Exp ext
  -- ..

Edit: Please close is that is the case

Last edited 9 months ago by Iceland_jack (previous) (diff)

comment:2 in reply to:  1 Changed 9 months ago by RyanGlScott

Resolution: invalid
Status: newclosed

Replying to Iceland_jack:

Please close is that is the case

You got it. :)

comment:3 Changed 9 months ago by Iceland_jack

Great, could GHC detect that ETag -> Type is an instance (don't know the right terminology) of WithAnyTag and propose quantifying over it?

    • Expected kind ‘WithAnyTag’, but ‘ext1’ has kind ‘ETag -> *’
    • In the first argument of ‘Exp’, namely ‘ext’
      In the type ‘Exp ext’
      In the definition of data constructor ‘Var’
   |
17 |   Var :: ext VarTag -> Exp ext
   |                            ^^^
    • Try quantifying over `AnyTag`
   |
17 |   Var :: forall (ext::AnyTag). ext VarTag -> Exp ext
   |

comment:4 Changed 9 months ago by goldfire

Description: modified (diff)
Keywords: TypeInType TypeErrorMessages added
Summary: Higher-Rank Kinds work in ADT but not GADTError messages: suggest annotating with higher-rank kind

Yes, I suppose that wouldn't be too hard.

comment:5 Changed 9 months ago by goldfire

Resolution: invalid
Status: closednew
Note: See TracTickets for help on using tickets.