[GHC] #10432: panic with kind polymorphism

19 May 2015

      #10432: panic with kind polymorphism
-------------------------------------+-------------------------------------
              Reporter:  Ashley      |             Owner:
  Yakeley                            |            Status:  new
                  Type:  bug         |         Milestone:
              Priority:  normal      |           Version:  7.10.1
             Component:  Compiler    |  Operating System:  Unknown/Multiple
  (Type checker)                     |   Type of failure:  None/Unknown
              Keywords:              |        Blocked By:
          Architecture:              |   Related Tickets:
  Unknown/Multiple                   |
             Test Case:              |
              Blocking:              |
Differential Revisions:              |
-------------------------------------+-------------------------------------
 {{{#!hs
 {-# LANGUAGE ExistentialQuantification, PolyKinds,
 DataKinds, RankNTypes, GADTs, TypeOperators #-}
 module Bug where
 import Data.Type.Equality

 data WrappedType = forall a. WrapType a;

 matchReflK :: forall (a :: ka) (b :: kb) (r :: *).
   ('WrapType a :~: 'WrapType b) -> (('WrapType a ~ 'WrapType b) => r) ->
 r;
 matchReflK Refl r = r;
 }}}

 give this:

 {{{
 Bug.hs:8:15:
     Couldn't match kind ‘ka’ with ‘kb’
       ‘ka’ is untouchable
         inside the constraints ('WrapType a ~ 'WrapType b)
         bound by the type signature for
                    matchReflK :: ('WrapType a ~ 'WrapType b) => r
         at Bug.hs:(8,15)-(9,74)ghc: panic! (the 'impossible' happened)
   (GHC version 7.10.1 for x86_64-unknown-linux):
         No skolem info: ka_aqv[sk]

 Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug
 }}}

 I actually think GHC should accept this (and furthermore infer `ka ~ kb`).

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10432
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler