Ticket #7585: Bug.hs

File Bug.hs, 540 bytes (added by goldfire, 15 months ago)

triggers the bug

Line 
1{-# LANGUAGE GADTs, RankNTypes, KindSignatures, PolyKinds, TypeOperators, DataKinds,
2             TypeFamilies #-}
3
4module Bug where
5
6data SBool :: Bool -> * where
7  SFalse :: SBool False
8  STrue :: SBool True
9
10data SList :: [Bool] -> * where
11  SNil :: SList '[]
12  SCons :: SBool h -> SList t -> SList (h ': t)
13
14type family (a :: k) :==: (b :: k) :: Bool
15type instance where
16  '[] :==: '[] = True
17  (h1 ': t1) :==: (h2 ': t2) = True
18  a :==: b = False
19
20(%==%) :: SList ls1 -> SList ls2 -> SBool (ls1 :==: ls2)
21SNil %==% (SCons _ _) = SFalse