blob: b6f5d056b5342982fe3830e3e1e95736259481a7 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
{-# LANGUAGE TypeFamilies #-}
module Refl2 where
type family T (a :: * -> *) :: * -> *
data U a x = U (T a x)
mkU :: a x -> U a x
mkU x = U undefined
-- The first definition says "Could not deduce (T a x ~ T a x)", the other two
-- work fine
foo :: a x -> U a x
foo x = case mkU x of U t -> id (U t)
-- foo x = case mkU x of U t -> id ((U :: T a x -> U a x) t)
-- foo x = case mkU x of U t -> U t
|
