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

Tests for indexed type synonyms

The tests expose bugs in an implementation of indexed type families which
hasn't been pushed to the HEAD yet. They are all marked as expect_fail.
parent 64207639
{-# LANGUAGE TypeFamilies, FlexibleContexts #-}
-- Results in context reduction stack overflow
module Class1 where
class C a where
foo :: a x -> a y
class C (T a) => D a where
type T a :: * -> *
bar :: a -> T a x -> T a y
instance C Maybe where
foo Nothing = Nothing
instance D () where
type T () = Maybe
bar x t = foo t
{-# LANGUAGE TypeFamilies, GADTs, EmptyDataDecls #-}
-- This wrongly fails with
--
-- Can't construct the infinite type n = PLUS n ZERO
module GADT1 where
data ZERO
data SUCC n
data Nat n where
Zero :: Nat ZERO
Succ :: Nat n -> Nat (SUCC n)
type family PLUS m n
type instance PLUS ZERO n = n
type instance PLUS (SUCC m) n = SUCC (PLUS m n)
data EQUIV x y where
EQUIV :: EQUIV x x
plus_zero :: Nat n -> EQUIV (PLUS n ZERO) n
plus_zero Zero = EQUIV
plus_zero (Succ n) = case plus_zero n of
EQUIV -> EQUIV
{-# LANGUAGE TypeFamilies, GADTs #-}
-- Fails with
--
-- Couldn't match expected type `y' against inferred type `x'
module GADT2 where
data EQUAL x y where
EQUAL :: x~y => EQUAL x y
foo :: EQUAL x y -> x -> y
foo EQUAL x = x
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -fglasgow-exts #-}
-- Test infix type constructors in type families
module Infix where
type family x :+: y
type instance Int :+: Int = Int
......@@ -27,3 +27,11 @@ test('Records', normal, compile, [''])
#
test('NewTyCo', ignore_output, run_command, ['$MAKE NewTyCo'])
clean(['NewTyCo1.o', 'NewTyCo1.hi', 'NewTyCo2.o', 'NewTyCo2.hi'])
test('Infix', expect_fail, compile, [''])
test('GADT1', expect_fail, compile, [''])
test('GADT2', 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