blob: 4db7b62889e1812a31ba1366371bffbb6752b24a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
{-# LANGUAGE GADTs #-}
-- Trac #345
module ShouldCompile where
data Succ n
data Zero
class Plus x y z | x y -> z
instance Plus Zero x x
instance Plus x y z => Plus (Succ x) y (Succ z)
infixr 5 :::
data List :: * -> * -> * where
Nil :: List a Zero
(:::) :: a -> List a n -> List a (Succ n)
append :: Plus x y z => List a x -> List a y -> List a z
append Nil ys = ys
append (x ::: xs) ys = x ::: append xs ys
|
