[Haskell-cafe] GADT question

[oleg at pobox.com]

John Meacham wrote:

>  data Type = ForAll [TyVar] Rho   -- Forall type
>           | Fun    Type Type      -- Function type
>           | TyCon  TyCon          -- Type constants
>           | TyVar  TyVar          -- Always bound by a ForAll

> with the three synonyms and their constraints being

> type Sigma = Type
> type Rho   = Type       -- No top-level ForAll
> type Tau   = Type       -- No ForAlls anywhere

> I would like the type system to distinguish the three types and enforce
> their properties.

Perhaps the enclosed code might be of help. Tests:

	test1 = TyCon "Int"
	*Forall> :t test1
	test1 :: Type FANil

	test2 = Forall ["a"] (Fun (TyVar "a") (TyVar "a"))
	*Forall> :t test2
	test2 :: Type FATop

	-- Inferred type!
	test3 = Fun test2 test1
	*Forall> :t test3
	test3 :: Type FASomewhere

	test3' = Fun test1 test1
	*Forall> :t test3'
	test3' :: Type FANil

	test4 = Forall ["b"] test3
	*Forall> :t test4
	test4 :: Type FATop

	test4' = Forall ["b"] test2 -- Error!
        No instance for (RhoC FATop)
        arising from use of `Forall' at /tmp/m.hs:43:9-14

That is, in test4, the second argument of Forall is not of the type
rho! Typeclasses would work too. I'm lacking a good example to show
off this machinery...


{-# OPTIONS -fglasgow-exts #-}

module Forall where

data FANil
data FATop
data FASomewhere

type Id = String

type Tau = Type FANil

data Type a where
    Forall :: (RhoC a) => [Id] -> Type a -> Type FATop
    Fun    :: (FAMerge a b c) => Type a -> Type b -> Type c
    TyCon  :: Id -> Type FANil
    TyVar  :: Id -> Type FANil

type Sigma a = Type a
--type (RhoC a) => Rho a =   Type a -- I wish that worked...

class RhoC a
instance RhoC FANil
instance RhoC FASomewhere

class FAMerge a b c | a b -> c
instance FAMerge FANil FANil FANil
instance FAMerge FANil FASomewhere FASomewhere
instance FAMerge FANil FATop FASomewhere
instance FAMerge FATop       a FASomewhere
instance FAMerge FASomewhere a FASomewhere

test1 = TyCon "Int"
test2 = Forall ["a"] (Fun (TyVar "a") (TyVar "a"))
test3 = Fun test2 test1
test3' = Fun test1 test1

-- I guess we need to hide the data constructors of Type and use
-- functions like rho, fun, tycon, etc. to construct the values of
-- Type
rho :: (RhoC a) => Type a -> Type a
rho = id

test4 = Forall ["b"] test3
-- The following is error!
--test4' = Forall ["b"] test2