search

google-code-export / omega

Automatically exported from code.google.com/p/omega
Other
2 stars 0 forks source link

Problem with labelEq #5

Closed GoogleCodeExporter closed 9 years ago

GoogleCodeExporter commented 9 years ago 
The below transcript says it all:

prompt> labelEq `jj `jj

In the expression: labelEq `jj
the argument did not have type: Label a

We computed the Constructor `jj to have type Tag
We expected it to be *0

Different types
   Tag   !=   *0
(Tag,*0)
prompt> labelEq
<primfun labelEq> : forall a b.Label a -> Label b -> Maybe (Equal (Label a) 
(Label b))
prompt> labelEq `jj

In the expression: labelEq `jj
the argument did not have type: Label a

We computed the Constructor `jj to have type Tag
We expected it to be *0

Different types
   Tag   !=   *0
(Tag,*0)
prompt> `jjj
`jjj : Label `jjj

I guess the decl should be thus:

labelEq :: forall (a::Tag) (b::Tag).Label a -> Label b -> Maybe (Equal (Label 
a) (Label b))

Original issue reported on code.google.com by ggr...@gmail.com on 5 May 2007 at 10:34

GoogleCodeExporter commented 9 years ago 
One more improvement:

labelEq :: forall (a::Tag) (b::Tag).Label a -> Label b -> Maybe (EqTag a b)

Original comment by ggr...@gmail.com on 1 Jun 2007 at 11:42

GoogleCodeExporter commented 9 years ago 
Fixed in Omega 1.4.2:

prompt> labelEq `jj `jj
(Just Eq) : Maybe (Equal `jj `jj)
prompt> labelEq
<primfun labelEq> : forall (a:Tag) (b:Tag).Label a -> Label b -> Maybe (Equal a 
b)

Original comment by ggr...@gmail.com on 11 Jun 2007 at 2:35