search

google-code-export / omega

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

unification fails due to missing normalization #47

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/issue47-SetEmulatio
n.omg>
2. in the check> loop, enter ":norm {l=v; r}s"
3. check> :h
Hint = SingleLabel _e

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

observe that {l=v; r}s expression should be typeable as SingleLabel _e
however the unification fails:

check> :q
**** Near line: 59 column: 1

*** Error type checking match ***

(Ex (Just (l, v, r, eq, entire))) ->
   (Check {l=v;r}s)

***   type:
(exists ('g :: Tag) ('h :: *0) ('i :: Row Tag *0) .
        Maybe (Label 'g
              ,('h
               ,(SingleLabel 'i
                ,((Equal {exclude 'g 'i} 'i) ,(Equal RCons 'g 'h 'i _e) )
                )
               )
              )) -> SingleLabel _e

***   vars: entire:Equal {_b=_c; _d}r _e, eq:Equal {exclude _b _d} _d,
r:SingleLabel _d, v:_c, l:Label _b
*** truths: 

In the expression: More l v r
the result type: SingleLabel {_b=_c; _d}r
was not what was expected: SingleLabel _e
refinement: (_a,(Label _b,(_c,(SingleLabel _d,(Equal {exclude _b _d}
_d,Equal {_b=_c; _d}r _e)))))
truths:

(V) different types
   _e   !=   {_b=_c; f}r
(uk5,{smh=umh; gow}r)

My idea is that unification of variable with type constructor application
should do a normalization step first.

This is a follow-up to issue46 and the testcase has a fix to it as
prerequisite.

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

GoogleCodeExporter commented 9 years ago 
[deleted comment]
GoogleCodeExporter commented 9 years ago 
it helps to add

unifyVar (v@(Tv _ (Rigid _ _ _) _)) (x@(TyApp _ _)) = emit (TcTv v) x

before
unifyVar v t = matchErr "(V) different types" (TcTv v) t

This gets issue47-SetEmulation.omg loading :-)

The exact theory is not clear. An occur check is definitely needed (when 
occurring as argument to a type 
constructor).

Maybe we need to modify the algo that returns free variables to tell whether it 
appears inside of a type 
function.

Original comment by ggr...@gmail.com on 19 Dec 2007 at 9:50

GoogleCodeExporter commented 9 years ago 
revision 63.

the occurs check is very restrictive,
we have to reconsider the occurs check strategy,
when the occurrence is inside of type function application,
then occurrence should be allowed.

a == {f a}            -- OK
a == {f (Con a)}      -- OK
a == Con {f a}        -- OK
a == Con a            -- NOT OK

Original comment by ggr...@gmail.com on 20 Dec 2007 at 12:04

GoogleCodeExporter commented 9 years ago 
r495. See checkin comment, I would encourage a code review on this one ;-)

Might be a good fix.

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

GoogleCodeExporter commented 9 years ago 
as of 1.4.7pre, r502, the file still does not load:

Omega Interpreter: version 1.4.7pre
Build Date: unspecified

Type ':?' for command line help.
Loading source files = ["issue47-SetEmulation.omg"]
->Loading import issue47-SetEmulation.omg
->Loading import LangPrelude.prg
   <-LangPrelude.prg loaded.

**** Near File: issue47-SetEmulation.omg
line: 55 column: 1

No progress can be made on the term:
   {exclude _a _b}
No rule for exclude matched.
Either the rules are incomplete, or a lemma is needed.
<-issue47-SetEmulation.omg loaded.

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

GoogleCodeExporter commented 9 years ago 
maybe we need the splitClass fix (MutVar|Easy|Hard)

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