Ticket #1807: Test.hs

File Test.hs, 461 bytes (added by guest, 6 years ago)
Line 
1{-# LANGUAGE TypeFamilies, GADTs #-}
2module Test where
3
4data List n where
5    -- Works
6    --Cons :: (Maybe n ~ n') => List n -> List n'
7    --Cons :: (Maybe n ~ n', n' ~ Maybe n) => List n -> List n'
8
9    -- Fails
10    Cons :: (n' ~ Maybe n) => List n -> List n'
11    --Cons :: (n' ~ Maybe n, Maybe n ~ n') => List n -> List n'
12
13class Snoc i where
14    snoc :: List i -> List (Maybe i)
15
16instance Snoc i => Snoc (Maybe i) where
17    snoc (Cons xs) = Cons (snoc xs)