on master help sign in
Injectivity of type classes on LHS
49af6f9Edwin Brady
src/Idris/Elab/Term.hs+1−1
@@ -741,7 +741,7 @@ elab ist info emode opts fn tm
741 ns <- apply (Var f) (map isph args)
741 ns <- apply (Var f) (map isph args)
742-- trace ("ns is " ++ show ns) $ return ()
742-- trace ("ns is " ++ show ns) $ return ()
743 -- mark any type class arguments as injective
743 -- mark any type class arguments as injective
744− mapM_ checkIfInjective (map snd ns)
744+ when (not pattern) $ mapM_ checkIfInjective (map snd ns)
745 unifyProblems -- try again with the new information,
745 unifyProblems -- try again with the new information,
746 -- to help with disambiguation
746 -- to help with disambiguation
747 ulog <- getUnifyLog
747 ulog <- getUnifyLog