search

google-code-export / omega

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

Absurdity appears as truth in certain pattern matches #27

Open GoogleCodeExporter opened 9 years ago

GoogleCodeExporter commented 9 years ago 
I am not sure that this is a bug, but it definitely looks strange...

compile <http://svn.berlios.de/svnroot/repos/al4nin/trunk/found-bugs/issue27-
HenkTest.omg>

It shows an error:

**** Near line: 80 column: 1

While type checking in the scope of:
   tau (Bind (LV cl) (a@(Lit (Spine' 1v))) (b@Value)) = Bind cl a (tau b) 
We need to prove:
   Equal {discipline (Spine 1t) {climb (Binder 1t 0t)}} {climb {discipline (Spine 1t) (Binder 1t 0t)}}, 
Equal {discipline (Spine 1t) {climb (Binder 1t 0t)}} (Spine 1t)
From the truths:Climber' (Spine 1t),Equal 1t 0t,
And the rules:UP,LV,SE,Spine',Step,Base,S,Z,S,Z,
But, The equations: (Binder 1t 1t=Binder 1t 1t, Binder 1t 1t=Spine 1t) =>  have 
no solution

The part with "From the truths:Climber' (Spine 1t),Equal 1t 0t," looks absurd.
Looks like the combination of pattern matches makes the typechecker to
create an "Equal 1t 0t" truth. I doubt that this is very sound, since 
everything can be
deduced from absurdity.

Please tell me if you need this testcase reduced.

Original issue reported on code.google.com by ggr...@gmail.com on 13 Oct 2007 at 10:38