@@ -93,18 +93,27 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
93 show r) pats))
93 show r) pats))
94 ist <- get
94 ist <- get
95 let tcase = opt_typecase (idris_options ist)
95 let tcase = opt_typecase (idris_options ist)
96+ let pdef = map debind pats
96− let tree = simpleCase tcase (map debind pats)
97+ let tree = simpleCase tcase pdef
98+ tclift $ sameLength pdef
97 logLvl 3 (show tree)
99 logLvl 3 (show tree)
98 ctxt <- getContext
100 ctxt <- getContext
99 case lookupTy (namespace info) n ctxt of
101 case lookupTy (namespace info) n ctxt of
100 [ty] -> updateContext (addCasedef n (inlinable opts)
102 [ty] -> updateContext (addCasedef n (inlinable opts)
101− tcase (map debind pats) ty)
103+ tcase pdef ty)
102 [] -> return ()
104 [] -> return ()
104 debind (x, y) = (depat x, depat y)
106 debind (x, y) = (depat x, depat y)
105 depat (Bind n (PVar t) sc) = depat (instantiate (P Bound n t) sc)
107 depat (Bind n (PVar t) sc) = depat (instantiate (P Bound n t) sc)
106 depat x = x
108 depat x = x
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
108elabVal :: ElabInfo -> Bool -> PTerm -> Idris (Term, Type)
117elabVal :: ElabInfo -> Bool -> PTerm -> Idris (Term, Type)
109elabVal info aspat tm_in
118elabVal info aspat tm_in
110 = do ctxt <- getContext
119 = do ctxt <- getContext