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]

this somehow got duplicated

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

• Changed state: Duplicate

[GoogleCodeExporter]

see issue51

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

[GoogleCodeExporter]

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