@@ -162,30 +162,34 @@ addTyInferred n
162162 addDef n TIPartial (idris_tyinfodata i) }
163163
164164addTyInfConstraints :: [(Term, Term)] -> Idris ()
165−addTyInfConstraints ts = do -- iputStrLn (show ts)
166− mapM_ (addConstraint True) ts
165+addTyInfConstraints ts = do logLvl 2 $ "TI missing: " ++ show ts
166+ mapM_ addConstraint ts
167167 return ()
168− where addConstraint True (x, y) -- MV on the left
169− | (P _ mv _, args) <- unApply x
170− = do ist <- get
171− case lookup mv (idris_metavars ist) of
172− Just _ -> addConstraintRule mv y
173− _ -> addConstraint False (x, y)
174− addConstraint False (x, y)
175− | (P _ mv _, args) <- unApply y
176− = do ist <- get
177− case lookup mv (idris_metavars ist) of
178− Just _ -> addConstraintRule mv x
179− _ -> return ()
180− addConstraint _ _ = return () -- FIXME: report error?
168+ where addConstraint (x, y) = findMVApps x y
169+
170+ findMVApps x y
171+ = do let (fx, argsx) = unApply x
172+ let (fy, argsy) = unApply y
173+ if (not (fx == fy))
174+ then do
175+ tryAddMV fx y
176+ tryAddMV fy x
177+ else mapM_ addConstraint (zip argsx argsy)
178+
179+ tryAddMV (P _ mv _) y =
180+ do ist <- get
181+ case lookup mv (idris_metavars ist) of
182+ Just _ -> addConstraintRule mv y
183+ _ -> return ()
184+ tryAddMV _ _ = return ()
181185
182186 addConstraintRule :: Name -> Term -> Idris ()
183187 addConstraintRule n t
184188 = do ist <- get
185− logLvl 2 $ "TI constraint: " ++ show (n, t)
189+ logLvl 1 $ "TI constraint: " ++ show (n, t)
186190 case lookupCtxt n (idris_tyinfodata ist) of
187191 [TISolution ts] ->
188− do let ti' = addDef n (TISolution (ts ++ [t]))
192+ do let ti' = addDef n (TISolution (t : ts))
189193 (idris_tyinfodata ist)
190194 put $ ist { idris_tyinfodata = ti' }
191195 _ ->