[Agda] How do I handle haskell type contexts from agda when using the ffi?

[Chris Moline]

Hi, I'm making a binding to gtk to help me gain some familiarity  with the
language but I don't know how to reflect type constraints within agda. How
can I make "instances" of a type?

For example, 'actionConnectProxy :: (ActionClass self, WidgetClass proxy) =>
self -> proxy -> IO ()'

This is easily exported with



postulate
  actionConnectProxy : {A, B : Set} -> A -> B -> IO Unit

{-# COMPILED actionConnectProxy Graphics.UI.Gtk.actionConnectProxy #-}



But how do I restrict A to ActionClass and B to WidgetClass? I could go


postulate WidgetClass : {A : Set} -> A -> A

{-# COMPILED_TYPE WidgetClass (WidgetClass a => a) #-}



But  I would like the data type to be somehow restricted to "instances" of
the type. Any help would be appreciated.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130824/290ab786/attachment.html