Ticket #6018: Injective.hs
| File Injective.hs, 296 bytes (added by lunaris, 13 months ago) |
|---|
| Line | |
|---|---|
| 1 | {-# LANGUAGE TypeFamilies #-} |
| 2 | |
| 3 | module Injective where |
| 4 | |
| 5 | injective family F (a :: *) :: * |
| 6 | |
| 7 | type instance F Int = Bool |
| 8 | type instance F Bool = Int |
| 9 | |
| 10 | f :: F a -> F a |
| 11 | f x = x |
| 12 | |
| 13 | --g :: F Int -> F Int |
| 14 | g x = f x |
| 15 | |
| 16 | injective family G (a :: *) :: * |
| 17 | |
| 18 | type instance G a = a |
| 19 | |
| 20 | h :: G a -> G a |
| 21 | h = id |
| 22 | |
| 23 | i x = h x |
