search

google-code-export / omega

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

refinement failure with recursive Equal #48

Open GoogleCodeExporter opened 9 years ago

GoogleCodeExporter commented 9 years ago 
What steps will reproduce the problem?
1. load <http://svn.berlios.de/svnroot/repos/al4nin/trunk/found-bugs/issue48-
SetEmulation.omg>
2. observe error
**** Near line: 53 column: 1

While infering the type of the pattern: Eq
we expected it to have type: Equal {exclude _b _c} _c
but, the current refinement fails because _c != {exclude _b _c}.
Sometimes reordering the patterns can fix this.

What is the expected output? What do you see instead?

I would expect that refinement is possible for self-referential Equal types. 
When functions can 
return values of such types (see issue46) they should also accept them.

You probably need a fix to issue43 to see this specific error.

Original issue reported on code.google.com by ggr...@gmail.com on 13 Dec 2007 at 11:24

GoogleCodeExporter commented 9 years ago 
The error originates from Infer2.hs:1435

          ; thingsToUnify <- down tauExpect tauC
          ; eitherInfo <- mguStar vsC thingsToUnify
          ; case eitherInfo of
             Right(s,x,y) -> badRefine pat t s x y -- <<<<<<<<<<<
             Left(psi,truths) ->
               do { k2 <- addUnifier psi (addPVS vsC k)

Original comment by ggr...@gmail.com on 14 Dec 2007 at 12:33

GoogleCodeExporter commented 9 years ago 
revision 57. on branches/potentially-unsound

Original comment by ggr...@gmail.com on 14 Dec 2007 at 1:01

GoogleCodeExporter commented 9 years ago 
revision 58 is a cleanup.

57+58 are in the patch.

Original comment by ggr...@gmail.com on 18 Dec 2007 at 1:50

Attachments:

GoogleCodeExporter commented 9 years ago 
I do not think that the above patches are good.

Anyway, the error is different now:

**** Near File: issue48-SetEmulation.omg
line: 53 column: 1

While inferring the type of the pattern: Eq
we expected it to have type: Equal {exclude _b _c} _c
but we computed type: Equal _e _e
where types have kinds:
   _b:Tag
   _c:Row Tag *0
   _d:*1
   _e:_d
but, the current refinement fails because _c != {exclude _b _c}.
Sometimes reordering the patterns can fix this.

Original comment by ggr...@gmail.com on 12 Jan 2011 at 2:18