Opened 5 months ago

Last modified 5 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 Cc: goldfire
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 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 (4)

comment:1 Changed 5 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 5 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 5 months ago by crockeea

Description: modified (diff)

comment:4 Changed 5 months ago by simonpj

Keywords: TypeInType added
Note: See TracTickets for help on using tickets.