Re: [GHC] #13365: Kind-inference for poly-kinded GADTs

2 Mar 2017

      #13365: Kind-inference for poly-kinded GADTs
-------------------------------------+-------------------------------------
        Reporter:  crockeea          |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.0.1
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by RyanGlScott):

 * cc: goldfire (added)

Comment:

 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 **c**omplete, **u**ser-specified **k**ind **s**ignature (CUSK) for
 `C`. For reference, if you had typed this:

    {{{#!hs
    {-# 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.
 2. The error message is quite awful. The issue is with `a`, not `x`, so I
 don't know why GHC is complaining about `x`.

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13365#comment:1
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler