[GHC] #11711: Typechecker assertion failure

[GHC]

#11711: Typechecker assertion failure
-------------------------------------+-------------------------------------
           Reporter:  bgamari        |             Owner:
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.0.1
          Component:  Compiler       |           Version:  8.0.1-rc2
  (Type checker)                     |
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  Compile-time
  Unknown/Multiple                   |  crash
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 I've seen this program both fail with a typechecker assertion and Core
 lint violations with various GHC versions,
 {{{#!hs
 {-# 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

 }}}

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