data family Sing (k :: *) :: k -> *
type Sing' (x :: k) = Sing k x
data TyArr' (a :: *) (b :: *) :: *
type TyArr (a :: *) (b :: *) = TyArr' a b -> *
type family (a :: TyArr k1 k2) @@ (b :: k1) :: k2
data TyPi' (a :: *) (b :: TyArr a *) :: *
type TyPi (a :: *) (b :: TyArr a *) = TyPi' a b -> *
type family (a :: TyPi k1 k2) @@@ (b :: k1) :: k2 @@ b
$(return [])
data T (a :: *) (b :: *) where
T1 :: forall a. T a a
T2 :: forall a b. T a b -> T a (b, b)
data A (a :: *) (x :: TyArr' * *)
$(return [])
data B (a :: *) (x :: TyPi' * (A a))
$(return [])
data C (x :: TyArr' * *)
$(return [])
data D (x :: TyPi' * C)
$(return [])
type instance A a @@ x = *
$(return [])
type instance B a @@@ x = T a x
$(return [])
type instance C @@ a = TyPi * (A a)
$(return [])
type instance D @@@ a = B a
$(return [])
data instance Sing (T a b) x where
ST1 :: forall a. Sing (T a a) 'T1
ST2 :: forall (a :: *) (b :: *) (c :: D @@@ a @@@ b). Sing (T a (b, b)) ('T2 c)
produces
ghc: panic! (the 'impossible' happened)
(GHC version 7.11.20150527 for x86_64-unknown-linux):
ASSERT failed! file compiler/types/TyCoRep.hs, line 1817
From @RafaelBocquet, extracted from #31:
produces