git.iko.soy/Idris-dev
on master help sign in
Injectivity of type classes on LHS

We shouldn't do anything to resolve type classes on the LHS.

commit49af6f9b3e98932b5f1352ac9665d42b0a41e598 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 11 Jul 2015, 15:33 (11 years ago) parent12bd67b
1 file changed+1−1
compare with master
unifiedsplit
src/Idris/Elab/Term.hs+1−1
src/Idris/Elab/Term.hs+1−1
@@ -741,7 +741,7 @@ elab ist info emode opts fn tm
741741 ns <- apply (Var f) (map isph args)
742742-- trace ("ns is " ++ show ns) $ return ()
743743 -- mark any type class arguments as injective
744− mapM_ checkIfInjective (map snd ns)
744+ when (not pattern) $ mapM_ checkIfInjective (map snd ns)
745745 unifyProblems -- try again with the new information,
746746 -- to help with disambiguation
747747 ulog <- getUnifyLog