Commit 4945a1a2 authored by chak@cse.unsw.edu.au.'s avatar chak@cse.unsw.edu.au.
Browse files

Test for #1722

parent 3fb5d600
{-# LANGUAGE TypeFamilies, GADTs, PatternSignatures, KindSignatures, EmptyDataDecls #-}
module ShouldCompile where
data Typed
data Untyped
type family TU a b :: *
type instance TU Typed b = b
type instance TU Untyped b = ()
-- A type witness type, use eg. for pattern-matching on types
data Type a where
TypeInt :: Type Int
TypeBool :: Type Bool
TypeString :: Type String
TypeList :: Type t -> Type [t]
data Expr :: * -> * -> * {- tu a -} where
Const :: Type a -> a -> Expr tu (TU tu a)
Var2 :: String -> TU tu (Type a) -> Expr tu (TU tu a)
bug1 :: Expr Typed Bool -> ()
bug1 (Const TypeBool False) = ()
bug2a :: Expr Typed Bool -> ()
bug2a (Var2 "x" (TypeBool :: Type Bool)) = ()
bug2b :: Expr Typed (TU Typed Bool) -> ()
bug2b (Var2 "x" TypeBool) = ()
......@@ -58,6 +58,7 @@ test('GADT8', normal, compile, [''])
test('GADT9', normal, compile, [''])
test('GADT10', expect_fail, compile, [''])
test('GADT11', normal, compile, [''])
test('GADT12', expect_fail, compile, [''])
test('Class1', normal, compile, [''])
test('Class2', normal, compile, [''])
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment