[Agda] Agda equalType variation

[Remi Turk]

Hi everybody,

for my master thesis I am creating a GRIN/EHC [1, 2] back end for
Agda. In the EHC back end, `main' has essentially the type
"World -> Int", and IO is based on a reader monad model.

Of course, I want to abstract away from that in my prelude, so I
define an abstract type IO, and don't export World:

> abstract
>     private
>         postulate
>             World : Set
> 
>     {-# BUILTIN WORLD World #-}
> 
>     IO      : Set -> Set
>     IO a    = World -> a

and builtin integers:

> postulate
>     Int : Set
> 
> {-# BUILTIN INTEGER Int #-}


Then, `main' is supposed to get this type signature

> main : IO Int

However, when I define IO abstract, I can no longer use

	equalType :: (MonadTCM tcm) => Type -> Type -> tcm Constraints

to check whether main has the right type, because equalType
cannot see through "abstract".

So my question is, is there a variation of equalType that _is_ able
to see through abstract types?

With kind regards, Remi

[1] http://www.cs.chalmers.se/~boquist/phd/
[2] http://www.cs.uu.nl/wiki/Ehc/WebHome