1269791 · Idris-dev · git.iko.soy

src/Idris/AbsSyntax.hs+14−12

@@ -853,7 +853,7 @@ expandParams dec ps ns infs tm = en tm

853853 | n `elem` (map fst ps ++ ns) && t /= Placeholder

854854 = let n' = mkShadow n in

855855 PDPair f p (PRef f' n') (en t) (en (shadow n n' r))

856− en (PEq f l r) = PEq f (en l) (en r)

856+ en (PEq f lt rt l r) = PEq f (en lt) (en r) (en l) (en r)

857857 en (PRewrite f l r g) = PRewrite f (en l) (en r) (fmap en g)

858858 en (PTyped l r) = PTyped (en l) (en r)

859859 en (PPair f p l r) = PPair f p (en l) (en r)

@@ -1022,7 +1022,7 @@ getPriority i tm = 1 -- pri tm

10221022 pri (PTrue _ _) = 0

10231023 pri (PFalse _) = 0

10241024 pri (PRefl _ _) = 1

1025− pri (PEq _ l r) = max 1 (max (pri l) (pri r))

1025+ pri (PEq _ _ _ l r) = max 1 (max (pri l) (pri r))

10261026 pri (PRewrite _ l r _) = max 1 (max (pri l) (pri r))

10271027 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))

10281028 pri (PAppBind _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))

@@ -1096,8 +1096,6 @@ addUsingConstraints syn fc t

10961096 let ns = namesIn [] ist t

10971097 let cs = getConstraints t -- check declared constraints

10981098 let addconsts = uconsts \\ cs

1099− -- if all names in the arguments of addconsts appear in ns,

1100− -- add the constraint implicitly

11011099 return (doAdd addconsts ns t)

11021100 where uconsts = filter uconst (using syn)

11031101 uconst (UConstraint _ _) = True

@@ -1191,7 +1189,8 @@ getUnboundImplicits i sc tm = []

11911189-- argument position.

11921190

11931191-- This has become a right mess already. Better redo it some time...

1194−

1192+-- TODO: This is obsoleted by the new way of elaborating types, but there's still

1193+-- a couple of places which use it. Clean them up!

11951194implicit :: ElabInfo -> SyntaxInfo -> Name -> PTerm -> Idris PTerm

11961195implicit info syn n ptm = implicit' info syn [] n ptm

11971196

@@ -1288,7 +1287,7 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

12881287 put (PTacImplicit 10 l n scr Placeholder : decls,

12891288 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

12901289 imps True (n:env) sc

1291− imps top env (PEq _ l r)

1290+ imps top env (PEq _ _ _ l r)

12921291 = do (decls, ns) <- get

12931292 let isn = namesIn uvars ist l ++ namesIn uvars ist r

12941293 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

@@ -1357,10 +1356,12 @@ addImpl' inpat env infns ist ptm

13571356 | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat qq ist fc f ds []

13581357 ai qq env ds (PHidden (PRef fc f))

13591358 | not (f `elem` map fst env) = handleErr $ aiFn inpat False qq ist fc f ds []

1360− ai qq env ds (PEq fc l r)

1361− = let l' = ai qq env ds l

1359+ ai qq env ds (PEq fc lt rt l r)

1360+ = let lt' = ai qq env ds lt

1361+ rt' = ai qq env ds rt

1362+ l' = ai qq env ds l

13621363 r' = ai qq env ds r in

1363− PEq fc l' r'

1364+ PEq fc lt' rt' l' r'

13641365 ai qq env ds (PRewrite fc l r g)

13651366 = let l' = ai qq env ds l

13661367 r' = ai qq env ds r

@@ -1698,7 +1699,8 @@ matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where

16981699 | not names && (not (isConName n (tt_ctxt i) ||

16991700 isFnName n (tt_ctxt i)) || tm == Placeholder)

17001701 = return [(n, tm)]

1701− match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'

1702+ match (PEq _ _ _ l r) (PEq _ _ _ l' r')

1703+ = do ml <- match' l l'

17021704 mr <- match' r r'

17031705 return (ml ++ mr)

17041706 match (PRewrite _ l r _) (PRewrite _ l' r' _)

@@ -1789,7 +1791,7 @@ substMatchShadow n shs tm t = sm shs t where

17891791 | otherwise = PPi p x (sm xs t) (sm (x : xs) sc)

17901792 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)

17911793 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)

1792− sm xs (PEq f x y) = PEq f (sm xs x) (sm xs y)

1794+ sm xs (PEq f xt yt x y) = PEq f (sm xs xt) (sm xs yt) (sm xs x) (sm xs y)

17931795 sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)

17941796 (fmap (sm xs) tm)

17951797 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)

@@ -1813,7 +1815,7 @@ shadow n n' t = sm t where

18131815 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)

18141816 sm (PAppBind f x as) = PAppBind f (sm x) (map (fmap sm) as)

18151817 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)

1816− sm (PEq f x y) = PEq f (sm x) (sm y)

1818+ sm (PEq f xt yt x y) = PEq f (sm xt) (sm yt) (sm x) (sm y)

18171819 sm (PRewrite f x y tm) = PRewrite f (sm x) (sm y) (fmap sm tm)

18181820 sm (PTyped x y) = PTyped (sm x) (sm y)

18191821 sm (PPair f p x y) = PPair f p (sm x) (sm y)

src/Idris/AbsSyntaxTree.hs+20−18

@@ -681,7 +681,7 @@ data PTerm = PQuote Raw

681681 | PFalse FC -- ^ _|_

682682 | PRefl FC PTerm

683683 | PResolveTC FC

684− | PEq FC PTerm PTerm -- ^ Equality type: A = B

684+ | PEq FC PTerm PTerm PTerm PTerm -- ^ Heterogeneous equality type: A = B

685685 | PRewrite FC PTerm PTerm (Maybe PTerm)

686686 | PPair FC PunInfo PTerm PTerm

687687 | PDPair FC PunInfo PTerm PTerm PTerm

@@ -723,7 +723,7 @@ mapPT f t = f (mpt t) where

723723 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)

724724 mpt (PAppBind fc t as) = PAppBind fc (mapPT f t) (map (fmap (mapPT f)) as)

725725 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)

726− mpt (PEq fc l r) = PEq fc (mapPT f l) (mapPT f r)

726+ mpt (PEq fc lt rt l r) = PEq fc (mapPT f lt) (mapPT f rt) (mapPT f l) (mapPT f r)

727727 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)

728728 mpt (PPair fc p l r) = PPair fc p (mapPT f l) (mapPT f r)

729729 mpt (PDPair fc p l t r) = PDPair fc p (mapPT f l) (mapPT f t) (mapPT f r)

@@ -1086,7 +1086,7 @@ eqDecl = PDatadecl eqTy (piBindp impl [(n "A", PType), (n "B", PType)]

10861086 pimp (n "B") Placeholder False,

10871087 pexp (PRef bi (n "x")),

10881088 pexp (PRef bi (n "x"))])), bi, [])]

1089− where n a = sMN 0 a

1089+ where n a = sUN a

10901090 reflDoc = parseDocstring . T.pack $

10911091 "A proof that `x` in fact equals `x`. To construct this, you must have already " ++

10921092 "shown that both sides are in fact equal."

@@ -1096,7 +1096,7 @@ eqDecl = PDatadecl eqTy (piBindp impl [(n "A", PType), (n "B", PType)]

10961096eqParamDoc = [(n "A", parseDocstring . T.pack $ "the type of the left side of the equality"),

10971097 (n "B", parseDocstring . T.pack $ "the type of the right side of the equality")

10981098 ]

1099− where n a = sMN 0 a

1099+ where n a = sUN a

11001100

11011101eqOpts = []

11021102

@@ -1242,7 +1242,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

12421242 rbrace <+> text "->" </> prettySe 10 ((n, True):bnd) sc

12431243 prettySe p bnd (PApp _ (PRef _ f) args) -- normal names, no explicit args

12441244 | UN nm <- basename f

1245− , not (ppopt_impl ppo) && null (getExps args) =

1245+ , not (ppopt_impl ppo) && null (getShowArgs args) =

12461246 prettyName True (ppopt_impl ppo) bnd f

12471247 prettySe p bnd (PAppBind _ (PRef _ f) [])

12481248 | not (ppopt_impl ppo) = text "!" <> prettyName True (ppopt_impl ppo) bnd f

@@ -1250,14 +1250,16 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

12501250 | UN nm <- basename op

12511251 , not (tnull nm) &&

12521252 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =

1253− case getExps args of

1253+ case getShowArgs args of

12541254 [] -> opName True

1255− [x] -> group (opName True <$> group (prettySe 0 bnd x))

1255+ [x] -> group (opName True <$> group (prettySe 0 bnd (getTm x)))

12561256 [l,r] -> let precedence = fromMaybe 20 (fmap prec f)

1257− in bracket p precedence $ inFix l r

1258− (l:r:rest) -> bracket p 1 $

1259− enclose lparen rparen (inFix l r) <+>

1260− align (group (vsep (map (prettyArgSe bnd) rest)))

1257+ in bracket p precedence $ inFix (getTm l) (getTm r)

1258+ (l@(PExp _ _ _ _) : r@(PExp _ _ _ _) : rest) ->

1259+ bracket p 1 $

1260+ enclose lparen rparen (inFix (getTm l) (getTm r)) <+>

1261+ align (group (vsep (map (prettyArgS bnd) rest)))

1262+ as -> opName True <+> align (vsep (map (prettyArgS bnd) as))

12611263 where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op

12621264 f = getFixity (opStr op)

12631265 left l = case f of

@@ -1299,7 +1301,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

12991301 prettySe p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"

13001302 prettySe p bnd (PTrue _ TypeOrTerm) = text "()"

13011303 prettySe p bnd (PFalse _) = annName falseTy $ text "_|_"

1302− prettySe p bnd (PEq _ l r) =

1304+ prettySe p bnd (PEq _ _ _ l r) =

13031305 bracket p 2 . align . group $

13041306 prettySe 10 bnd l <+> eq <$> group (prettySe 10 bnd r)

13051307 where eq = annName eqTy (text "=")

@@ -1596,7 +1598,7 @@ instance Sized PTerm where

15961598 size (PFalse fc) = 1

15971599 size (PRefl fc _) = 1

15981600 size (PResolveTC fc) = 1

1599− size (PEq fc left right) = 1 + size left + size right

1601+ size (PEq fc _ _ left right) = 1 + size left + size right

16001602 size (PRewrite fc left right _) = 1 + size left + size right

16011603 size (PPair fc _ left right) = 1 + size left + size right

16021604 size (PDPair fs _ left ty right) = 1 + size left + size ty + size right

@@ -1634,7 +1636,7 @@ allNamesIn tm = nub $ ni [] tm

16341636 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

16351637 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc

16361638 ni env (PHidden tm) = ni env tm

1637− ni env (PEq _ l r) = ni env l ++ ni env r

1639+ ni env (PEq _ _ _ l r) = ni env l ++ ni env r

16381640 ni env (PRewrite _ l r _) = ni env l ++ ni env r

16391641 ni env (PTyped l r) = ni env l ++ ni env r

16401642 ni env (PPair _ _ l r) = ni env l ++ ni env r

@@ -1659,7 +1661,7 @@ boundNamesIn tm = nub $ ni tm

16591661 ni (PLam n ty sc) = n : (ni ty ++ ni sc)

16601662 ni (PLet n ty val sc) = n : (ni ty ++ ni val ++ ni sc)

16611663 ni (PPi p n ty sc) = niTacImp p ++ (n : (ni ty ++ ni sc))

1662− ni (PEq _ l r) = ni l ++ ni r

1664+ ni (PEq _ _ _ l r) = ni l ++ ni r

16631665 ni (PRewrite _ l r _) = ni l ++ ni r

16641666 ni (PTyped l r) = ni l ++ ni r

16651667 ni (PPair _ _ l r) = ni l ++ ni r

@@ -1695,7 +1697,7 @@ implicitNamesIn uvars ist tm = nub $ ni [] tm

16951697 \\ nub (concatMap (ni env) (map fst os)))

16961698 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

16971699 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc

1698− ni env (PEq _ l r) = ni env l ++ ni env r

1700+ ni env (PEq _ _ _ l r) = ni env l ++ ni env r

16991701 ni env (PRewrite _ l r _) = ni env l ++ ni env r

17001702 ni env (PTyped l r) = ni env l ++ ni env r

17011703 ni env (PPair _ _ l r) = ni env l ++ ni env r

@@ -1728,7 +1730,7 @@ namesIn uvars ist tm = nub $ ni [] tm

17281730 \\ nub (concatMap (ni env) (map fst os)))

17291731 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

17301732 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc

1731− ni env (PEq _ l r) = ni env l ++ ni env r

1733+ ni env (PEq _ _ _ l r) = ni env l ++ ni env r

17321734 ni env (PRewrite _ l r _) = ni env l ++ ni env r

17331735 ni env (PTyped l r) = ni env l ++ ni env r

17341736 ni env (PPair _ _ l r) = ni env l ++ ni env r

@@ -1759,7 +1761,7 @@ usedNamesIn vars ist tm = nub $ ni [] tm

17591761 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)

17601762 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

17611763 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc

1762− ni env (PEq _ l r) = ni env l ++ ni env r

1764+ ni env (PEq _ _ _ l r) = ni env l ++ ni env r

17631765 ni env (PRewrite _ l r _) = ni env l ++ ni env r

17641766 ni env (PTyped l r) = ni env l ++ ni env r

17651767 ni env (PPair _ _ l r) = ni env l ++ ni env r

src/Idris/CaseSplit.hs+2−2

@@ -231,7 +231,7 @@ replaceVar ctxt n t (PApp fc f pats) = PApp fc f (map substArg pats)

231231 subst (PApp fc (PRef _ t) pats)

232232 | isTConName t ctxt = Placeholder -- infer types

233233 subst (PApp fc f pats) = PApp fc f (map substArg pats)

234− subst (PEq fc l r) = Placeholder -- PEq fc (subst l) (subst r)

234+ subst (PEq fc _ _ l r) = Placeholder -- PEq fc (subst l) (subst r)

235235 subst x = x

236236

237237 substArg arg = arg { getTm = subst (getTm arg) }

@@ -349,7 +349,7 @@ getClause l fn fp

349349 getNameFrom i used (PPi _ _ _ _)

350350 = uniqueNameFrom (mkSupply [sUN "f", sUN "g"]) used

351351 getNameFrom i used (PApp fc f as) = getNameFrom i used f

352− getNameFrom i used (PEq _ _ _) = uniqueNameFrom [sUN "prf"] used

352+ getNameFrom i used (PEq _ _ _ _ _) = uniqueNameFrom [sUN "prf"] used

353353 getNameFrom i used (PRef fc f)

354354 = case getNameHints i f of

355355 [] -> uniqueName (sUN "x") used

src/Idris/DSL.hs+3−2

@@ -39,7 +39,8 @@ expandDo dsl (PAppBind fc t args) = PAppBind fc (expandDo dsl t)

3939 (map (fmap (expandDo dsl)) args)

4040expandDo dsl (PCase fc s opts) = PCase fc (expandDo dsl s)

4141 (map (pmap (expandDo dsl)) opts)

42−expandDo dsl (PEq fc l r) = PEq fc (expandDo dsl l) (expandDo dsl r)

42+expandDo dsl (PEq fc lt rt l r) = PEq fc (expandDo dsl lt) (expandDo dsl rt)

43+ (expandDo dsl l) (expandDo dsl r)

4344expandDo dsl (PPair fc p l r) = PPair fc p (expandDo dsl l) (expandDo dsl r)

4445expandDo dsl (PDPair fc p l t r) = PDPair fc p (expandDo dsl l) (expandDo dsl t)

4546 (expandDo dsl r)

@@ -98,7 +99,7 @@ var dsl n t i = v' i t where

9899 v' i (PTyped l r) = PTyped (v' i l) (v' i r)

99100 v' i (PApp f x as) = PApp f (v' i x) (fmap (fmap (v' i)) as)

100101 v' i (PCase f t as) = PCase f (v' i t) (fmap (pmap (v' i)) as)

101− v' i (PEq f l r) = PEq f (v' i l) (v' i r)

102+ v' i (PEq f lt rt l r) = PEq f (v' i lt) (v' i rt) (v' i l) (v' i r)

102103 v' i (PPair f p l r) = PPair f p (v' i l) (v' i r)

103104 v' i (PDPair f p l t r) = PDPair f p (v' i l) (v' i t) (v' i r)

104105 v' i (PAlternative a as) = PAlternative a $ map (v' i) as

src/Idris/DeepSeq.hs+1−1

@@ -205,7 +205,7 @@ instance NFData PTerm where

205205 rnf (PFalse x1) = rnf x1 `seq` ()

206206 rnf (PRefl x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

207207 rnf (PResolveTC x1) = rnf x1 `seq` ()

208− rnf (PEq x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

208+ rnf (PEq x1 x2 x3 x4 x5) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

209209 rnf (PRewrite x1 x2 x3 x4)

210210 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

211211 rnf (PPair x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

src/Idris/Delaborate.hs+68−9

@@ -12,8 +12,9 @@ import Idris.Core.Evaluate

1212import Idris.Docstrings (overview, renderDocstring)

1313import Idris.ErrReverse

1414

15−import Data.List (intersperse)

15+import Data.List (intersperse, nub)

1616import qualified Data.Text as T

17+import Control.Monad.State

1718

1819import Debug.Trace

1920

@@ -96,9 +97,10 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

9697 | n == sUN "Sigma"

9798 = PDPair un IsType (PRef un x) (de env [] ty)

9899 (de ((x,x):env) [] (instantiate (P Bound x ty) r))

99− deFn env (P _ n _) [_,_,l,r]

100+ deFn env (P _ n _) [lt,rt,l,r]

100101 | n == pairCon = PPair un IsTerm (de env [] l) (de env [] r)

101− | n == eqTy = PEq un (de env [] l) (de env [] r)

102+ | n == eqTy = PEq un (de env [] lt) (de env [] rt)

103+ (de env [] l) (de env [] r)

102104 | n == sUN "Sg_intro" = PDPair un IsTerm (de env [] l) Placeholder

103105 (de env [] r)

104106 deFn env f@(P _ n _) args

@@ -165,9 +167,10 @@ pprintErr' i (InternalMsg s) =

165167 text ("Please consider reporting at " ++ bugaddr)

166168 ]

167169pprintErr' i (CantUnify _ x_in y_in e sc s) =

168− let (x, y) = addImplicitDiffs (delab i x_in) (delab i y_in) in

169− text "Can't unify" <> indented (annTm x_in (pprintTerm' i (map (\ (n, b) -> (n, False)) sc) x)) <$>

170− text "with" <> indented (annTm y_in (pprintTerm' i (map (\ (n, b) -> (n, False)) sc) y)) <>

170+ let (x_ns, y_ns) = renameMNs x_in y_in

171+ (x, y) = addImplicitDiffs (delab i x_ns) (delab i y_ns) in

172+ text "Can't unify" <> indented (annTm x_ns (pprintTerm' i (map (\ (n, b) -> (n, False)) sc) x)) <$>

173+ text "with" <> indented (annTm y_ns (pprintTerm' i (map (\ (n, b) -> (n, False)) sc) y)) <>

171174 case e of

172175 Msg "" -> empty

173176 _ -> line <> line <> text "Specifically:" <>

@@ -263,6 +266,41 @@ pprintErr' i (ReflectionFailed msg err) =

263266 indented (pprintErr' i err) <>

264267 text ("This is probably a bug. Please consider reporting it at " ++ bugaddr)

265268

269+-- Make sure the machine invented names are shown helpfully to the user, so

270+-- that any names which differ internally also differ visibly

271+-- FIXME: I can't actually contrive an error to test this! Will revisit later...

272+renameMNs :: Term -> Term -> (Term, Term)

273+renameMNs x y = let ns = nub $ allTTNames x ++ allTTNames y

274+ newnames = execState getRenames (zip ns ns) in

275+ (rename newnames x, rename newnames y)

276+ where

277+ getRenames :: State [(Name, Name)] ()

278+ getRenames = do getRs x; getRs y

279+

280+ getRs :: Term -> State [(Name, Name)] ()

281+ getRs (P _ n@(MN i x) _) = do

282+ nmap <- get

283+ when (n `notElem` map fst nmap) $

284+ put $ (n, uniqueName n (map fst nmap)) : nmap

285+ getRs (App f a) = do getRs f; getRs a

286+ getRs (Bind n b sc) = do

287+ nmap <- get

288+ when (n `notElem` map fst nmap) $

289+ put $ (n, uniqueName n (map fst nmap)) : nmap

290+ getRs sc

291+ getRs t = return ()

292+

293+ rename :: [(Name, Name)] -> Term -> Term

294+ rename ns (P nt x t) | Just x' <- lookup x ns = P nt x' t

295+ rename ns (App f a) = App (rename ns f) (rename ns a)

296+ rename ns (Bind x b sc)

297+ = let b' = fmap (rename ns) b

298+ sc' = rename ns sc in

299+ case lookup x ns of

300+ Just x' -> Bind x' b' sc'

301+ Nothing -> Bind x b' sc'

302+ rename ns x = x

303+

266304-- If the two terms only differ in their implicits, mark the implicits which

267305-- differ as AlwaysShow so that they appear in errors

268306addImplicitDiffs :: PTerm -> PTerm -> (PTerm, PTerm)

@@ -295,10 +333,30 @@ addImplicitDiffs x y

295333 addI (PRefl fc a) (PRefl fc' b)

296334 = let (a', b') = addI a b in

297335 (PRefl fc a', PRefl fc' b')

298− addI (PEq fc a b) (PEq fc' c d)

336+ addI (PEq fc at bt a b) (PEq fc' ct dt c d)

337+ | trace (show (at,bt)) False = undefined

338+ | at `expLike` ct && bt `expLike` dt

299339 = let (a', c') = addI a c

300340 (b', d') = addI b d in

301− (PEq fc a' b', PEq fc' c' d')

341+ (PEq fc at bt a' b', PEq fc' ct dt c' d')

342+ | otherwise

343+ = let (at', ct') = addI at ct

344+ (bt', dt') = addI bt dt

345+ (a', c') = addI a c

346+ (b', d') = addI b d

347+ showa = if at `expLike` ct then [] else [AlwaysShow]

348+ showb = if bt `expLike` dt then [] else [AlwaysShow] in

349+ (PApp fc (PRef fc eqTy) [(pimp (sUN "A") at' True)

350+ { argopts = showa },

351+ (pimp (sUN "B") bt' True)

352+ { argopts = showb },

353+ pexp a', pexp b'],

354+ PApp fc (PRef fc eqTy) [(pimp (sUN "A") ct' True)

355+ { argopts = showa },

356+ (pimp (sUN "B") dt' True)

357+ { argopts = showb },

358+ pexp c', pexp d'])

359+

302360 addI (PPair fc pi a b) (PPair fc' pi' c d)

303361 = let (a', c') = addI a c

304362 (b', d') = addI b d in

@@ -321,7 +379,8 @@ addImplicitDiffs x y

321379 = n == n' && expLike s s' && expLike t t'

322380 expLike (PPair _ _ x y) (PPair _ _ x' y') = expLike x x' && expLike y y'

323381 expLike (PDPair _ _ x _ y) (PDPair _ _ x' _ y') = expLike x x' && expLike y y'

324− expLike (PEq _ x y) (PEq _ x' y') = expLike x x' && expLike y y'

382+ expLike (PEq _ xt yt x y) (PEq _ xt' yt' x' y')

383+ = expLike x x' && expLike y y'

325384 expLike (PRefl _ x) (PRefl _ x') = expLike x x'

326385 expLike x y = x == y

327386

src/Idris/ElabQuasiquote.hs+5−3

@@ -106,10 +106,12 @@ extractUnquotes (PCase fc expr cases)

106106extractUnquotes (PRefl fc x)

107107 = do (x', ex) <- extractUnquotes x

108108 return (PRefl fc x', ex)

109−extractUnquotes (PEq fc a b)

110− = do (a', ex1) <- extractUnquotes a

109+extractUnquotes (PEq fc at bt a b)

110+ = do (at', ex1) <- extractUnquotes at

111+ (bt', ex2) <- extractUnquotes bt

112+ (a', ex1) <- extractUnquotes a

111113 (b', ex2) <- extractUnquotes b

112− return (PEq fc a' b', ex1 ++ ex2)

114+ return (PEq fc at' bt' a' b', ex1 ++ ex2)

113115extractUnquotes (PRewrite fc x y z)

114116 = do (x', ex1) <- extractUnquotes x

115117 (y', ex2) <- extractUnquotes y

src/Idris/ElabTerm.hs+3−3

@@ -254,9 +254,9 @@ elab ist info emode opts fn tm

254254 elab' ina (PRefl fc t)

255255 = elab' ina (PApp fc (PRef fc eqCon) [pimp (sMN 0 "A") Placeholder True,

256256 pimp (sMN 0 "x") t False])

257− elab' ina (PEq fc l r) = elab' ina (PApp fc (PRef fc eqTy)

258− [pimp (sMN 0 "A") Placeholder True,

259− pimp (sMN 0 "B") Placeholder False,

257+ elab' ina (PEq fc lt rt l r) = elab' ina (PApp fc (PRef fc eqTy)

258+ [pimp (sUN "A") Placeholder True,

259+ pimp (sUN "B") Placeholder False,

260260 pexp l, pexp r])

261261 elab' ina@(_, a, inty, qq) (PPair fc _ l r)

262262 = do hnf_compute

src/Idris/IBC.hs+10−6

@@ -31,7 +31,7 @@ import Codec.Compression.Zlib (compress)

3131import Util.Zlib (decompressEither)

3232

3333ibcVersion :: Word8

34−ibcVersion = 74

34+ibcVersion = 75

3535

3636data IBCFile = IBCFile { ver :: Word8,

3737 sourcefile :: FilePath,

@@ -1406,10 +1406,12 @@ instance Binary PTerm where

14061406 put x2

14071407 PResolveTC x1 -> do putWord8 15

14081408 put x1

1409− PEq x1 x2 x3 -> do putWord8 16

1410− put x1

1411− put x2

1412− put x3

1409+ PEq x1 x2 x3 x4 x5 -> do putWord8 16

1410+ put x1

1411+ put x2

1412+ put x3

1413+ put x4

1414+ put x5

14131415 PRewrite x1 x2 x3 x4 -> do putWord8 17

14141416 put x1

14151417 put x2

@@ -1523,7 +1525,9 @@ instance Binary PTerm where

15231525 16 -> do x1 <- get

15241526 x2 <- get

15251527 x3 <- get

1526− return (PEq x1 x2 x3)

1528+ x4 <- get

1529+ x5 <- get

1530+ return (PEq x1 x2 x3 x4 x5)

15271531 17 -> do x1 <- get

15281532 x2 <- get

15291533 x3 <- get

src/Idris/IdrisDoc.hs+1−1

@@ -285,7 +285,7 @@ extractPTermNames (PMatchApp _ n) = [n]

285285extractPTermNames (PCase _ p ps) = let (ps1, ps2) = unzip ps

286286 in concatMap extract (p:(ps1 ++ ps2))

287287extractPTermNames (PRefl _ p) = extract p

288−extractPTermNames (PEq _ p1 p2) = concatMap extract [p1, p2]

288+extractPTermNames (PEq _ _ _ p1 p2) = concatMap extract [p1, p2]

289289extractPTermNames (PRewrite _ a b m) | Just c <- m =

290290 concatMap extract [a, b, c]

291291extractPTermNames (PRewrite _ a b _) = concatMap extract [a, b]

src/Idris/ParseOps.hs+1−1

@@ -38,7 +38,7 @@ table fixes

3838 ++ toTable (reverse fixes) ++

3939 [[backtick],

4040 [binary "$" (\fc x y -> flatten $ PApp fc x [pexp y]) AssocRight],

41− [binary "=" PEq AssocLeft]]

41+ [binary "=" (\fc x y -> PEq fc Placeholder Placeholder x y) AssocLeft]]

4242 where

4343 flatten :: PTerm -> PTerm -- flatten application

4444 flatten (PApp fc (PApp _ f as) bs) = flatten (PApp fc f (as ++ bs))

test/basic009/expected+1−1

@@ -1,5 +1,5 @@

11MAIN-PASS

22Faulty.idr:6:7:When elaborating type of Faulty.fault:

3−When elaborating an application of type constructor =:

3+When elaborating argument x to type constructor =:

44 Can't disambiguate name: A.num, B.C.num

55Multiple.idr:3:1:import alias not unique: "X"