search

cartazio / omega

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

constraints not properly reflected upon deconstruction #46

Open GoogleCodeExporter opened 8 years ago

GoogleCodeExporter commented 8 years ago 
What steps will reproduce the problem?
1. load <http://svn.berlios.de/svnroot/repos/al4nin/trunk/found-bugs/issue46-
SetEmulation.omg>
2. in the check> output enable
:set p
:set t
:set s
:set n

3. type :q and watch type checking failing:

...
But, The equations: (_g={exclude _b {exclude _b _d}}) =>  have no solution

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

I would expect that putting together a new data structure from the debris of an 
old one should 
succeed :-)

It prints

***    refinement: (_a,{_b=_c; {exclude _b _d}}r), (_d,{exclude _b _d}), 

before entering check>. The second part is the Equal constraint.

The Equal constraint on the More data constructor contributes to the 
refinement, but it is not 
accessible as evidence when building the result.
Maybe recursive refinement should contribute to the assumptions?

If (_d,{exclude _b _d} is a truth, then

(_g={exclude _b {exclude _b _d}})
becomes
(_g={exclude _b _d})
becomes
(_g=_d)
which is trivially true.

Original issue reported on code.google.com by ggr...@gmail.com on 12 Dec 2007 at 1:33

GoogleCodeExporter commented 8 years ago 
the issue may be void, I missed to declare "tail" to be existential in the 
signature.

With

apart :: SingleLabel row -> exists a v tail . Maybe (Label a, v, SingleLabel 
tail)
apart {}s = Ex Nothing
apart {l=v; rest}s = Ex (check (Just (l, v, rest)))

it *does* type check :-)

Original comment by ggr...@gmail.com on 12 Dec 2007 at 1:41

GoogleCodeExporter commented 8 years ago 
Since we want to re-assemble the original record later, we have to return the 
evidence.

Updated testcase to deal with the exists-problem, but returning Eq fails in a 
very similar way to the original 
description.

Original comment by ggr...@gmail.com on 12 Dec 2007 at 2:21

GoogleCodeExporter commented 8 years ago 
created branches/potentially-unsound from branches/typefun-pattern-issues

This is a field of experimentation now.

I proceed as proposed in this issue, by making assumptions out of the recursive
refinements (when rhs id a type function call).

Revision: 51 makes the testcase to compile.

Original comment by ggr...@gmail.com on 12 Dec 2007 at 3:00

GoogleCodeExporter commented 8 years ago 
Follow-on riddle:

<http://svn.berlios.de/svnroot/repos/al4nin/trunk/found-bugs/issue46b-SetEmulati
on.omg>

Original comment by ggr...@gmail.com on 12 Dec 2007 at 4:24

GoogleCodeExporter commented 8 years ago

Original comment by ggr...@gmail.com on 12 Dec 2007 at 8:31

GoogleCodeExporter commented 8 years ago 
the residual problem is now issue47

Original comment by ggr...@gmail.com on 13 Dec 2007 at 11:25

GoogleCodeExporter commented 8 years ago 
revision 64 cleans up some chatty output.

Original comment by ggr...@gmail.com on 20 Dec 2007 at 2:07