missing normalization in constraints

[GoogleCodeExporter]

Again I am not sure this is a bug, but I am stumped...

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

I get this error message:

**** Near line: 73 column: 1

While type checking: constfive
Under the truths: 
We tried to solve: LE {strat (Binder 1t 0t)} 1t
But we were left with: LE {strat (Binder 1t 0t)} 1t
The proposition: (LE {strat (Binder 1t 0t)} 1t) is refutable.

But using:

prompt> :no LE {strat (Binder 1t 0t)} 1t

   LE {strat (Binder 1t 0t)} 1t
Normalizes to:
  LE 0t 1t
Refinement:

I get something coherent. I guess that constraint checking should include 
normalization.

Original issue reported on code.google.com by ggr...@gmail.com on 14 Oct 2007 at 8:00

[GoogleCodeExporter]

[deleted comment]

[GoogleCodeExporter]

My humble guess is that solveConstraints (Infer2.hs:3646) is missing
a call to refine (Infer2.hs:3473), just after the lines

     ; let (oblig,residual) = splitR collected ([],[])
           assump = assumptions env -- Truths stored in the extended environment
           rules = getRules "" env
-- add this line
     ; (_, oblig') <- refine [] oblig rules   -- use oblig' instead of oblig from now on

I did not check if this even would compile...

Original comment by ggr...@gmail.com on 8 Nov 2007 at 9:16

[GoogleCodeExporter]

This modified function seems to do the trick:

solveConstraints :: ([Char],Rho) -> TcEnv -> [Pred] -> Mtc TcEnv Pred
([(TcTv,Tau)],[Pred],[Tau],[Tau])
solveConstraints (nm,rho) env rawCollected =
  do { -- Clean up first, eliminating type function calls and wipe out tautologies if
possible
     ; (_, collected) <- refine [] rawCollected [] -- rules and refinements to feed
in? what to do with refinements result?
     -- Split into Equalities and Relations, and normalize everything.
     ; let (oblig,residual) = splitR collected ([],[])
           assump = assumptions env -- Truths stored in the extended environment
           rules = getRules "" env
     ; (truths1,u0,_) <- inEnv env (liftNf normPredL assump)
     ; let oblig2 = foldr pred2Pair [] (subPred u0 oblig)
     ; (normOblig,u1,normTruths) <- inEnv env (normUnder truths1 oblig2)
     ; steps <- getBound "narrow" 25
     ; u2 <- handleM 2
                  (inEnv env (solveByNarrowing (3,steps) ("9."++nm,rho) normTruths
normOblig))
                  (underErr nm rules assump oblig)
     ; let u3 = u2 `o` (u1 `o` u0)
     ; expandTruths <- inEnv env (expandTruths2 (subPred u3 normTruths))
     ; (unsolved,un4) <- inEnv env (solvP expandTruths (map (subTau u3) residual))
     ; let u5 = un4 `o` u3
     ; let truths = (map (subTau u5) expandTruths)
           need = (map (subTau u5) residual)
     ; return(u5,unsolved,truths,need)}

Original comment by ggr...@gmail.com on 8 Nov 2007 at 10:50

[GoogleCodeExporter]

updated 
<http://svn.berlios.de/svnroot/repos/al4nin/trunk/found-bugs/issue28-HenkTest.om
g> to avoid 
secondary errors

Original comment by ggr...@gmail.com on 9 Nov 2007 at 4:19

[GoogleCodeExporter]

fixed in Thu, Nov 8, snapshot

Original comment by ggr...@gmail.com on 9 Nov 2007 at 7:00

• Changed state: Accepted

[GoogleCodeExporter]

Original comment by ggr...@gmail.com on 9 Nov 2007 at 7:01

• Changed state: Fixed