Ticket #1807: Test.hs
| File Test.hs, 461 bytes (added by guest, 6 years ago) |
|---|
| Line | |
|---|---|
| 1 | {-# LANGUAGE TypeFamilies, GADTs #-} |
| 2 | module Test where |
| 3 | |
| 4 | data 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 | |
| 13 | class Snoc i where |
| 14 | snoc :: List i -> List (Maybe i) |
| 15 | |
| 16 | instance Snoc i => Snoc (Maybe i) where |
| 17 | snoc (Cons xs) = Cons (snoc xs) |
