ggreif / omega

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

type inference in patterns with GADTs fails #39

Open GoogleCodeExporter opened 9 years ago

GoogleCodeExporter commented 9 years ago
What steps will reproduce the problem?
1. load this file:
<http://svn.berlios.de/svnroot/repos/al4nin/trunk/found-bugs/issue39-DejaVu.omg>
2. observe error message:
**** Near line: 80 column: 1
Non type constructor: _b as range of constructor: Ahh

3. When I enter the pattern part as an expression, it works:
prompt> Cons (Stop Ahh) Nil
[(Stop Ahh)]l : Thrist DejaVu () (Test Int)

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

I would expect that the pattern gets accepted

Still happens with the Nov 8 snapshot.

Original issue reported on code.google.com by ggr...@gmail.com on 17 Nov 2007 at 9:35

GoogleCodeExporter commented 9 years ago
More research.

this simplified function also fails:

deja'' :: Thrist DejaVu () [a] -> Thrist DejaVu () [a]
deja'' (t@(Cons (Stop []) Nil)) = t

this one finally loads:

deja'' :: Thrist DejaVu () [a] -> Thrist DejaVu () [a]
deja'' (t@(Cons (Stop _) Nil)) = t

Original comment by ggr...@gmail.com on 17 Nov 2007 at 10:45

GoogleCodeExporter commented 9 years ago
Getting closer:

deja'' :: DejaVu () (Test a) -> DejaVu () (Test a)
deja'' (t@Stop Ahh) = t

This also compiles, and is very similar to the testcase. The wrapping in Thrist 
seems to make the difference.

Testcase is updated.

Original comment by ggr...@gmail.com on 17 Nov 2007 at 11:06

GoogleCodeExporter commented 9 years ago

Original comment by ggr...@gmail.com on 6 Dec 2007 at 1:35

GoogleCodeExporter commented 9 years ago
a tentative fix is at r38.

please review, especially the unify with (Star level 0) part.
I am not at all sure that this fix is right :-/

patch attached

Original comment by ggr...@gmail.com on 6 Dec 2007 at 11:05

Attachments:

GoogleCodeExporter commented 9 years ago

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