regression with type inference

[GoogleCodeExporter]

What steps will reproduce the problem?
1. load
<http://svn.berlios.de/svnroot/repos/al4nin/trunk/found-bugs/issue49.omg>
into trunk-built 1.4.2+ snapshot
2. observe error:
**** Near line: 17 column: 1

While infering the type of the pattern: Nil
we expected it to have type: List' _c _d _e
but, the current refinement fails (No Match) because Nat != List b.
Sometimes reordering the patterns can fix this.

3. try the same with release 1.4.2, ---> no problems.

What is the expected output? What do you see instead?
This is a regression relative to release 1.4.2.
Occurs in the Nov 8 shapshot.

Original issue reported on code.google.com by ggr...@gmail.com on 17 Dec 2007 at 2:22

[GoogleCodeExporter]

instrumenting

checkBndrs rename mod f0 ps result =
  do { outputString (">>>>>>>>>>>>>> checkBndrs rho: " ++ shtt result)
     ; (frag,ps,ts,rng) <- checkBs rename mod f0 ps result
     ; return(frag,ps,ts,rng)}

gives us:

(TyApp
 (TyApp
  (Con (->)@1 %Ox)
  (TyApp
   (TyApp
    (TyApp (Con List'@1 %Ox)
       (Rigid 1206:(Star 1)))
    (Rigid 1207:(TyVar x1169::(Star 1))))
   (Rigid 1208:(Con Nat@2 %Ox))))
 (TyApp
  (Con Nat'@1 %Ox)
  (Rigid 1207:(TyVar x1169::(Star 1)))))

This seems to be the signature of len'.

Original comment by ggr...@gmail.com on 17 Dec 2007 at 2:50

[GoogleCodeExporter]

Of course this signature is wrong, (Con Nat@2) should be the second argument to 
(Con
List'@1) and not the third.

Now looking for callers of checkBndrs.

Called fron 2 places: fragForPs and typeExp(Lam)

fragForPs is it.

typeMatchPs calls fragForPs.

-------------------------vvv
checkDec mutRecFrag (mod,rho,Fun loc nm hint ms,skols) = newLoc loc $
  do { let frag = (markLambda (addSkol skols mutRecFrag))
     ; outputString ("77777: rho " ++ shtt rho ++ "\n77777: show " ++ show rho)

from

inferBndr:

  inferBndr renm frag1 ds | all isValFunPat ds =
    do { let decs = useTypeSig ds
       ; (frag2,triples) <- getDecTyp renm decs -- Step 1
       ; outputString ("8888888: triples: " ++ show triples)
       ; frag3 <-  frag2 +++ frag1
       ; ds2 <- mapM (checkDec frag3) triples   -- Step 2
       ; frag4 <- genFrag frag3
       ; return(simpleSigma unitT,frag4,ds2)
       }

The bug candidate is getDecTyp.

Original comment by ggr...@gmail.com on 17 Dec 2007 at 3:28

[GoogleCodeExporter]

tracked down a bit more:

checkPT loc pt =
  do { tenv <- getTypeEnv
     ; (levels,sigma) <-
           case pt of
             (PolyLevel vs t) -> do { us <- freshLevels vs; return(us,t) }
             other -> return ([],other)
     ; (snMap,names,eqns,rho) <- inferConSigma levels tenv loc ([],sigma)
     ; outputString ("checkPT:  rho: " ++ shtt rho)
     ; let s = Forall (windup names (eqns,rho))
     ; outputString ("checkPT:  s: " ++ shtt s)
     ; handleM 2 (check s (Star LvZero)) (errX pt) -- check the translation has kind *0
     ; (nameMap,skol) <- rigid snMap names []      -- build the mappings
     ; outputString ("checkPT:  nameMap: " ++ show nameMap)
     ; rho2 <- sub (nameMap,[],[],[]) rho          -- make fresh Rho
     ; outputString ("checkPT:  rho2: " ++ shtt rho2)
     ; eqn2 <- sub (nameMap,[],[],[]) eqns         -- and fresh equations
     ; return (s,(rho2,eqn2,skol))}
 where  rigid ((s,nm):xs) ((nm2,k,q):ys) subst =
            do { k2 <- sub (subst,[],[],[]) k   -- in explicit foralls, earlier may bind
               ; v <- newRigidTyVar q loc s k2  -- later, so we need to apply subst to k
               ; subst2 <- compX [(nm,TcTv v)] subst
               ; (subst3,skols) <- rigid xs ys subst2
               ; newname <- registerDisp s v    -- Update the Display to map the ridgid to the PT name
               ; return(subst3,v:skols)}
        rigid _ _ subst = return(subst,[])
        err s = failD 2 [Ds "The prototype:  ",Dd pt,Ds "\ndoes not have kind *0, because ",Ds s]

rho, s are looking good, nameMap is reasonable, rho2 looks strange.

Original comment by ggr...@gmail.com on 17 Dec 2007 at 10:50

[GoogleCodeExporter]

The definition of rigid in checkPT (Infer2.hs:1753) must be fixed. See below.

Rationale: inferConSigma returns an snMap and the names of forall-ed variables.
However the latter can contain more quantifiers that classify higher levels
of the variables in the snMap. The additional clause to rigid strips away
these extra variables from higher level.

-----------------------------------------------------------------------------
 where  rigid (snMap@((_,nm):_)) ((nm2,_,_):ys) subst | nm /= nm2 = rigid snMap ys subst
        rigid ((s,nm):xs) ((_,k,q):ys) subst =
            do { k2 <- sub (subst,[],[],[]) k   -- in explicit foralls, earlier may bind
               ; v <- newRigidTyVar q loc s k2  -- later, so we need to apply subst to k
               ; subst2 <- compX [(nm,TcTv v)] subst
               ; (subst3,skols) <- rigid xs ys subst2
               ; newname <- registerDisp s v    -- Update the Display to map the
ridgid to the PT name
               ; return(subst3,v:skols)}
        rigid _ _ subst = return(subst,[])

Original comment by ggr...@gmail.com on 18 Dec 2007 at 1:16

• Changed state: Started
• Added labels: Patch-imminent

[GoogleCodeExporter]

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

[GoogleCodeExporter]

checked in as revision 59, on branches/potentially-unsound.

This is the best I have now.

The fix is pretty straightforward. No unsoundness introduced here.

kyagrd, please check out this branch, it should work for you. If not,
please tell me. I shall test your whole program as soon as I have access
to your mail (this evening).

Original comment by ggr...@gmail.com on 18 Dec 2007 at 1:43

• Added labels: Patch-included
• Removed labels: Patch-imminent

Attachments:

• issue49.diff