Commit 3fb5d600 authored by chak@cse.unsw.edu.au.'s avatar chak@cse.unsw.edu.au.
Browse files

Test from #1815

parent 4e0d8dc6
{-# LANGUAGE TypeFamilies, GADTs, RankNTypes, EmptyDataDecls #-}
module ShouldCompile where
data Z
data S a
type family Sum n m
type instance Sum n Z = n
type instance Sum n (S m) = S (Sum n m)
data Nat n where
NZ :: Nat Z
NS :: (S n ~ sn) => Nat n -> Nat sn
data EQ a b = forall q . (a ~ b) => Refl
zerol :: Nat n -> EQ n (Sum Z n)
zerol NZ = Refl
zerol (NS n) = case zerol n of Refl -> Refl
......@@ -57,6 +57,7 @@ test('GADT7', expect_fail, compile, [''])
test('GADT8', normal, compile, [''])
test('GADT9', normal, compile, [''])
test('GADT10', expect_fail, compile, [''])
test('GADT11', normal, 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