[GHC] #12698: GHC panic on pattern synonym

[GHC]

#12698: GHC panic on pattern synonym
-------------------------------------+-------------------------------------
           Reporter:  Iceland_jack   |             Owner:
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.1
           Keywords:                 |  Operating System:  Unknown/Multiple
  PatternSynonyms                    |
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 {{{#!hs
 {-# Language ViewPatterns, TypeOperators, KindSignatures, PolyKinds,
 TypeInType, StandaloneDeriving, GADTs, RebindableSyntax, RankNTypes,
 LambdaCase, PatternSynonyms, TypeApplications #-}

 import GHC.Types
 import Prelude hiding ( fromInteger )
 import Data.Type.Equality
 import Data.Kind
 import qualified Prelude

 class Ty (a :: k) where ty :: T a
 instance Ty Int where ty = TI
 instance Ty Bool where ty = TB
 instance Ty a => Ty [a] where ty = TA TL ty
 instance Ty [] where ty = TL
 instance Ty (,) where ty = TP

 data AppResult (t :: k) where
   App :: T a -> T b -> AppResult (a b)

 data T :: forall k. k -> Type where
   TI :: T Int
   TB :: T Bool
   TL :: T []
   TP :: T (,)
   TA :: T f -> T x -> T (f x)
 deriving instance Show (T a)

 splitApp :: T a -> Maybe (AppResult a)
 splitApp = \case
   TI -> Nothing
   TB -> Nothing
   TL -> Nothing
   TP -> Nothing
   TA f x -> Just (App f x)

 data (a :: k1) :~~: (b :: k2) where
   HRefl :: a :~~: a

 eqT :: T a -> T b -> Maybe (a :~~: b)
 eqT a b =
   case (a, b) of
     (TI, TI) -> Just HRefl
     (TB, TB) -> Just HRefl
     (TL, TL) -> Just HRefl
     (TP, TP) -> Just HRefl

 pattern List :: () => [] ~~ b => T b
 pattern List <- (eqT (ty @(Type -> Type) @[]) -> Just HRefl)
   where List = ty

 pattern Int :: () => Int ~~ b => T b
 pattern Int <- (eqT (ty @Type @Int) -> Just HRefl)
   where Int = ty

 pattern (:<->:) :: () => fx ~ f x => T f -> T x -> T fx
 pattern f :<->: x <- (splitApp -> Just (App f x))
   where f :<->: x = TA f x

 pattern Foo <- List :<->: Int
 }}}

 Using GHCi version 8.1.20160930:

 {{{
 G$ ./ghc-stage2 -ignore-dot-ghci --interactive /tmp/td2W.hs
 GHCi, version 8.1.20160930: http://www.haskell.org/ghc/  :? for help
 [1 of 1] Compiling Main             ( /tmp/td2W.hs, interpreted )
 ghc-stage2: panic! (the 'impossible' happened)
   (GHC version 8.1.20160930 for x86_64-unknown-linux):
         ASSERT failed!
   k1_a2mO
   k1_a2mO
   [TCvSubst
      In scope: InScope {k_a2mM fx_a2mN f_a2mP x_a2mQ rep_a2ny r_a2nz
                         scrut_a2nB $cshowsPrec_a2ob $cshow_a2p1
 $cshowList_a2p8 $cty_a2pi
                         $cty_a2po $cty_a2pw $cty_a2pJ $cty_a2pP splitApp
 eqT $fTy(->)(,)
                         $fTy(->)[] $fTyTYPE[] $fTyTYPEBool $fTyTYPEInt
 $fShowT $mList
                         $bList $mInt $bInt $m:<->: $b:<->:}
      Type env: [a2mN :-> fx_a2mN, a2mP :-> f_a2mP, a2mQ :-> x_a2mQ,
                 a2nz :-> r_a2nz]
      Co env: []]
   Call stack:
       CallStack (from HasCallStack):
         prettyCurrentCallStack, called at
 compiler/utils/Outputable.hs:1076:58 in ghc:Outputable
         callStackDoc, called at compiler/utils/Outputable.hs:1125:22 in
 ghc:Outputable
         assertPprPanic, called at compiler/types/TyCoRep.hs:2318:46 in
 ghc:TyCoRep
   Call stack:
       CallStack (from HasCallStack):
         prettyCurrentCallStack, called at
 compiler/utils/Outputable.hs:1076:58 in ghc:Outputable
         callStackDoc, called at compiler/utils/Outputable.hs:1080:37 in
 ghc:Outputable
         pprPanic, called at compiler/utils/Outputable.hs:1123:5 in
 ghc:Outputable
         assertPprPanic, called at compiler/types/TyCoRep.hs:2318:46 in
 ghc:TyCoRep

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

 >
 }}}

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