Opened 9 months ago

Last modified 2 months ago

#13365 new bug

Kind-inference for poly-kinded GADTs

Reported by: crockeea Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.0.1
Keywords: TypeInType, CUSKs Cc: goldfire
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: #14139, #14207 Differential Rev(s):
Wiki Page:

Description (last modified by crockeea)

With -XPolyKinds, GADTs require kind signatures where they should be inferred. Moreover, the error when these kind sigs are omitted is baffling.

{-# LANGUAGE PolyKinds, GADTs #-}

import GHC.TypeLits

data Foo
  (x :: k)
  a
  where
    C1 :: (KnownNat x) => a -> Foo x a
    C2 :: a -> Foo Int a
error:
  • Expected kind ‘k’, but ‘x1’ has kind ‘Nat’
  • In the first argument of ‘Foo’, namely ‘x’
    In the type ‘Foo x a’
    In the definition of data constructor ‘C1’

From this error, I would never expect that putting a kind signature on a would help here. But a signature shouldn't be required at all: it's clear from the GADT constructors that a :: *.

Change History (8)

comment:1 Changed 9 months ago by RyanGlScott

Cc: goldfire added

I think there are actually two problems here:

  1. The fact that this doesn't typecheck. I think this is a known limitation of type inference having to do with the fact that you didn't give a complete, user-specified kind signature (CUSK) for C. For reference, if you had typed this:
{-# LANGUAGE PolyKinds, GADTs #-}

import GHC.TypeLits

data C
  (x :: k)
  (a :: k2)
  where
    C1 :: (KnownNat x) => a -> C x a
    C2 :: a -> C Int a

Then it works. I'll cc goldfire, out preeminent expert on CUSKs, to be sure.

  1. The error message is quite awful. The issue is with a, not x, so I don't know why GHC is complaining about x.

comment:2 Changed 9 months ago by goldfire

Ryan nailed it. This is a CUSK issue. When you have a CUSK, inference runs quite differently from when you don't. The error message is actually correct, given that we're doing non-CUSK inference here. What would be better is an NB: Adding a complete user-specified kind signature might help. Not clear how easy or hard it would be to know when to add the NB.

comment:3 Changed 9 months ago by crockeea

Description: modified (diff)

comment:4 Changed 8 months ago by simonpj

Keywords: TypeInType added

comment:5 Changed 3 months ago by goldfire

Keywords: CUSKs added

comment:6 Changed 3 months ago by RyanGlScott

comment:7 Changed 3 months ago by simonpj

See also #14139 for another example.

comment:8 Changed 2 months ago by RyanGlScott

#14207 is another example.

Note: See TracTickets for help on using tickets.