Commit f656d8a5 authored by rl@cse.unsw.edu.au's avatar rl@cse.unsw.edu.au
Browse files

Another indexed type families test

As before, this is against a patch which isn't in the HEAD yet.
parent 4e4d35bf
{-# LANGUAGE TypeFamilies, GADTs, EmptyDataDecls #-}
-- Panics in bind_args
module GADT3 where
data EQUAL x y where
EQUAL :: x~y => EQUAL x y
data ZERO
data SUCC n
data Nat n where
Zero :: Nat ZERO
Succ :: Nat n -> Nat (SUCC n)
type family PLUS n :: * -> *
type instance PLUS ZERO n = n
plus_zero :: Nat n -> EQUAL (PLUS ZERO n) n
plus_zero Zero = EQUAL
plus_zero (Succ n) = EQUAL
data FOO n where
FOO_Zero :: FOO ZERO
foo :: Nat m -> Nat n -> FOO n -> FOO (PLUS m n)
foo Zero n s = case plus_zero n of EQUAL -> s
...@@ -32,6 +32,7 @@ test('Infix', expect_fail, compile, ['']) ...@@ -32,6 +32,7 @@ test('Infix', expect_fail, compile, [''])
test('GADT1', expect_fail, compile, ['']) test('GADT1', expect_fail, compile, [''])
test('GADT2', expect_fail, compile, ['']) test('GADT2', expect_fail, compile, [''])
test('GADT3', expect_fail, compile, [''])
test('Class1', expect_fail, compile, ['']) test('Class1', expect_fail, compile, [''])
Markdown is supported
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