[GHC] #10432: panic with kind polymorphism

[GHC]

#10432: panic with kind polymorphism
-------------------------------------+-------------------------------------
        Reporter:  Ashley Yakeley    |                Owner:
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  7.10.1
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
-------------------------------------+-------------------------------------

Comment (by jstolarek):

 I'm using a compiler built by `./validate` from commit
 e2b579e8d77357e8b36f57d15daead101586ac8e and here's what I get for
 originally reported code:

 {{{
 [killy at xerxes : /dane/projekty/ghc/ghc-tests/types/T10432] cat T10432.hs
 {-# LANGUAGE ExistentialQuantification, PolyKinds,
 DataKinds, RankNTypes, GADTs, TypeOperators #-}
 module T10432 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;

 [killy at xerxes : /dane/projekty/ghc/ghc-tests/types/T10432] ghc-validate-
 stage1 -c -dcore-lint T10432.hs

 T10432.hs:8:15: error:
     Could not deduce: ka ~ kb
     from the context: 'WrapType a ~ 'WrapType b
       bound by the type signature for:
                  matchReflK :: ('WrapType a ~ 'WrapType b) => r
       at T10432.hs:(8,15)-(9,74)
     ‘ka’ is a rigid type variable bound by
          the type signature for:
            matchReflK :: 'WrapType a :~: 'WrapType b
                          -> (('WrapType a ~ 'WrapType b) => r) -> r
          at T10432.hs:8:15
     ‘kb’ is a rigid type variable bound by
          the type signature for:
            matchReflK :: 'WrapType a :~: 'WrapType b
                          -> (('WrapType a ~ 'WrapType b) => r) -> r
          at T10432.hs:8:15
     Expected type: 'WrapType b
       Actual type: 'WrapType a
     In the ambiguity check for the type signature for ‘matchReflK’:
       matchReflK :: forall (ka :: BOX) (kb :: BOX) (a :: ka) (b :: kb) r.
                     'WrapType a :~: 'WrapType b
                     -> (('WrapType a ~ 'WrapType b) => r) -> r
     To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
     In the type signature for ‘matchReflK’:
       matchReflK :: forall (a :: ka) (b :: kb) (r :: *).
                     (WrapType a :~: WrapType b)
                     -> ((WrapType a ~ WrapType b) => r) -> r
 }}}

 And for the code in comment:1:

 {{{
 [killy at xerxes : /dane/projekty/ghc/ghc-tests/types/T10432] cat T10432.hs
 {-# LANGUAGE ExistentialQuantification, PolyKinds,
 DataKinds, RankNTypes, GADTs, TypeOperators #-}
 module T10432 where
 import Data.Type.Equality

 data WrappedType = forall a. WrapType a;

 matchReflK2 :: forall (a :: ka) (b :: kb) (r :: *).
               ('WrapType a :~: 'WrapType b) ->  r
 matchReflK2 x
  = let foo :: ('WrapType a ~ 'WrapType b) => r
        foo = undefined
    in undefined

 [killy at xerxes : /dane/projekty/ghc/ghc-tests/types/T10432] ghc-validate-
 stage1 -c -dcore-lint T10432.hs
 [killy at xerxes : /dane/projekty/ghc/ghc-tests/types/T10432]
 }}}

 I have no idea why are we getting different behaviours :-/

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/10432#comment:4>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler