GADTs and functional dependencies

[Chris Kuklewicz]

You cannot create a normal function "fun".  You can make a type class function

fun :: Class a b => GADT a -> b

> data GADT a where
>      GADT :: GADT ()
>      GADT2 :: GADT String
> 
> -- fun1 :: GADT () -> () -- infers type
> fun1 g = case g of
>            (GADT :: GADT ()) -> ()
> 
> -- fun2 :: GADT String -> Bool -- infers type
> fun2 g = case g of
>            (GADT2 :: GADT String) -> True
> 
> -- "fun" cannot type check.  The type of 'g' cannot be both "GADT ()" and "GADT String"
> -- This is because "fun" is not a member of type class.
> {- 
> fun g = case g of
>            (GADT :: GADT ()) -> ()
>            (GADT2 :: GADT String) -> True
> -}
> 
> class Class a b | a -> b where
>   fun :: GADT a -> b
> 
> instance Class () () where
>   fun GADT = ()
> 
> instance Class String Bool where
>   fun GADT2 = True
> 
> main = print $ (fun GADT, fun GADT2) == ( (), True )
>