Typechecker assertion failure
I've seen this program both fail with a typechecker assertion and Core lint violations with various GHC versions,
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE TypeInType #-}
module Hi where
import Data.Kind (Type)
data (:~~:) a b where
HRefl :: a :~~: a
data TypeRep (a :: k) where
TrTyCon :: String -> TypeRep k -> TypeRep (a :: k)
TrApp :: forall k1 k2 (a :: k1 -> k2) (b :: k1).
TypeRep (a :: k1 -> k2)
-> TypeRep (b :: k1)
-> TypeRep (a b)
class Typeable (a :: k) where
typeRep :: TypeRep a
data TypeRepX where
TypeRepX :: forall k (a :: k). TypeRep a -> TypeRepX
eqTypeRep :: TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep = undefined
typeRepKind :: forall k (a :: k). TypeRep a -> TypeRep k
typeRepKind = undefined
funResultTy :: TypeRepX -> TypeRepX -> Maybe TypeRepX
funResultTy (TypeRepX f) (TypeRepX x)
| Just HRefl <- (typeRep :: TypeRep Type) `eqTypeRep` typeRepKind f
, TRFun arg res <- f
, Just HRefl <- arg `eqTypeRep` x
= Just (TypeRepX res)
| otherwise
= Nothing
trArrow :: TypeRep (->)
trArrow = undefined
pattern TRFun :: forall fun. ()
=> forall arg res. (fun ~ (arg -> res))
=> TypeRep arg
-> TypeRep res
-> TypeRep fun
pattern TRFun arg res <- TrApp (TrApp (eqTypeRep trArrow -> Just HRefl) arg) res
The most recent type checker error is,
$ ~/ghc/ghc-testing/inplace/bin/ghc-stage2 -dcore-lint ~/Hi.hs
[1 of 1] Compiling Hi ( /home/ben/Hi.hs, /home/ben/Hi.o )
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.1.20160315 for x86_64-unknown-linux):
tcTyVarDetails cobox_a1Nm :: k_a1N4[ssk] ~# Type
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
Trac metadata
Trac field | Value |
---|---|
Version | 8.0.1-rc2 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |