@@ -93,18 +93,27 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
9393 show r) pats))
9494 ist <- get
9595 let tcase = opt_typecase (idris_options ist)
96− let tree = simpleCase tcase (map debind pats)
96+ let pdef = map debind pats
97+ let tree = simpleCase tcase pdef
98+ tclift $ sameLength pdef
9799 logLvl 3 (show tree)
98100 ctxt <- getContext
99101 case lookupTy (namespace info) n ctxt of
100102 [ty] -> updateContext (addCasedef n (inlinable opts)
101− tcase (map debind pats) ty)
103+ tcase pdef ty)
102104 [] -> return ()
103105 where
104106 debind (x, y) = (depat x, depat y)
105107 depat (Bind n (PVar t) sc) = depat (instantiate (P Bound n t) sc)
106108 depat x = x
107109
110+ sameLength ((x, _) : xs)
111+ = do l <- sameLength xs
112+ let (f, as) = unApply x
113+ if (null xs || l == length as) then return (length as)
114+ else tfail (At fc (Msg "Clauses have differing numbers of arguments "))
115+ sameLength [] = return 0
116+
108117elabVal :: ElabInfo -> Bool -> PTerm -> Idris (Term, Type)
109118elabVal info aspat tm_in
110119 = do ctxt <- getContext