panic with kind polymorphism
{-# 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
).
Trac metadata
Trac field | Value |
---|---|
Version | 7.10.1 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |