restrictive occurs test with data constructor arguments

[GoogleCodeExporter]

What steps will reproduce the problem?
1. load
<//svn.berlios.de/svnroot/repos/al4nin/trunk/found-bugs/issue51-SetEmulation.omg
>
2. observe "Occurs check"
3.

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

I would expect that this compiles. Again we have a fixpoint in typefun
evaluation, which should be admissible.

Here is the exact error:

**** Near line: 48 column: 1

In the expression: Eq
the result type: level d . forall (c:*(1+d)) (e:c:*(1+d)).Equal e e
was not what was expected: Equal {exclude `a b} b
refinement: 
truths:

Occurs check
   b   !=   {exclude `a b}
(zgz,{exclude `a zgz})

Original issue reported on code.google.com by ggr...@gmail.com on 20 Dec 2007 at 10:04

[GoogleCodeExporter]

looks like unifyVar should special case
for self-referential typefun calls.

For these a predicate could be emitted.

Original comment by ggr...@gmail.com on 20 Dec 2007 at 10:19

• Changed state: Started

[GoogleCodeExporter]

a possible fix is in revision 62.

Original comment by ggr...@gmail.com on 20 Dec 2007 at 10:21

• Added labels: Patch-intended

[GoogleCodeExporter]

Issue 52 has been merged into this issue.

Original comment by ggr...@gmail.com on 13 Feb 2009 at 2:41

[GoogleCodeExporter]

As of r502 the specified file loads and behaves correctly.

Original comment by ggr...@gmail.com on 4 Jan 2011 at 3:10

• Changed state: Fixed