Injectivity assumptions

Parameters should only be assumed to be injective if they also happen to
be type class parameters, otherwise some things will type check which
otherwise shouldn't.

src/Idris/Elab/Clause.hs

@@ -543,7 +543,10 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
         let fn_is = case lookupCtxt fname (idris_implicits i) of
                          [t] -> t
                          _ -> []
-        let params = getParamsInType i [] fn_is (normalise ctxt [] fn_ty)
+        let norm_ty = normalise ctxt [] fn_ty
+        let params = getParamsInType i [] fn_is norm_ty
+        let tcparams = getTCParamsInType i [] fn_is norm_ty
+
         let lhs = mkLHSapp $ stripLinear i $ stripUnmatchable i $
                     propagateParams i params fn_ty (addImplPat i lhs_in)
 --         let lhs = mkLHSapp $ 
@@ -634,7 +637,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
                     (do pbinds ist lhs_tm
                         -- proof search can use explicitly written names
                         mapM_ addPSname (allNamesIn lhs_in)
-                        mapM_ setinj (nub (params ++ inj))
+                        mapM_ setinj (nub (tcparams ++ inj))
                         setNextName
                         (ElabResult _ _ is ctxt' newDecls highlights) <-
                           errAt "right hand side of " fname

src/Idris/Elab/Utils.hs

@@ -16,6 +16,7 @@ import Control.Applicative hiding (Const)
 import Control.Monad.State
 import Control.Monad
 import Data.List
+import Data.Maybe
 import qualified Data.Traversable as Traversable
 
 import Debug.Trace
@@ -211,6 +212,24 @@ getParamsInType i env ps t = let fix = getFixedInType i env ps t
                                  flex = getFlexInType i env fix t in
                                  [x | x <- fix, not (x `elem` flex)]
 
+getTCinj i (Bind n (Pi _ t _) sc) 
+    = getTCinj i t ++ getTCinj i (instantiate (P Bound n t) sc)
+getTCinj i ap@(App _ f a)
+    | (P _ n _, args) <- unApply ap,
+      isTCName n = mapMaybe getInjName args
+    | otherwise = []
+  where
+    isTCName n = case lookupCtxtExact n (idris_classes i) of
+                      Just _ -> True
+                      _ -> False
+    getInjName t | (P _ x _, _) <- unApply t = Just x
+                 | otherwise = Nothing
+getTCinj _ _ = []
+
+getTCParamsInType :: IState -> [Name] -> [PArg] -> Type -> [Name]
+getTCParamsInType i env ps t = let params = getParamsInType i env ps t
+                                   tcs = nub $ getTCinj i t in
+                                   filter (flip  elem tcs) params
 paramNames args env [] = []
 paramNames args env (p : ps)
    | length args > p = case args!!p of