@@ -164,19 +164,19 @@ pvars ist _ = []
164164getFixedInType i env (PExp _ _ _ _ : is) (Bind n (Pi _ t _) sc)
165165 = nub $ getFixedInType i env [] t ++
166166 getFixedInType i (n : env) is (instantiate (P Bound n t) sc)
167− ++ case t of
168− P _ n _ -> if n `elem` env then [n] else []
167+ ++ case unApply t of
168+ (P _ n _, _) -> if n `elem` env then [n] else []
169169 _ -> []
170170getFixedInType i env (_ : is) (Bind n (Pi _ t _) sc)
171171 = getFixedInType i (n : env) is (instantiate (P Bound n t) sc)
172172getFixedInType i env is tm@(App _ f a)
173173 | (P _ tn _, args) <- unApply tm
174− = case lookupCtxt tn (idris_datatypes i) of
175− [t] -> nub $ paramNames args env (param_pos t) ++
176− getFixedInType i env is f ++
177− getFixedInType i env is a
178− [] -> nub $ getFixedInType i env is f ++
179− getFixedInType i env is a
174+ = case lookupCtxtExact tn (idris_datatypes i) of
175+ Just t -> nub $ paramNames args env (param_pos t) ++
176+ getFixedInType i env is f ++
177+ getFixedInType i env is a
178+ Nothing -> nub $ getFixedInType i env is f ++
179+ getFixedInType i env is a
180180 | otherwise = nub $ getFixedInType i env is f ++
181181 getFixedInType i env is a
182182getFixedInType i _ _ _ = []
@@ -187,17 +187,16 @@ getFlexInType i env ps (Bind n (Pi _ t _) sc)
187187
188188getFlexInType i env ps tm@(App _ f a)
189189 | (P nt tn _, args) <- unApply tm, nt /= Bound
190− = case lookupCtxt tn (idris_datatypes i) of
191− [t] -> nub $ paramNames args env [x | x <- [0..length args],
192− not (x `elem` param_pos t)]
190+ = case lookupCtxtExact tn (idris_datatypes i) of
191+ Just t -> nub $ paramNames args env [x | x <- [0..length args],
192+ not (x `elem` param_pos t)]
193193 ++ getFlexInType i env ps f ++
194194 getFlexInType i env ps a
195− [] -> let ppos = case lookupCtxtName tn (idris_fninfo i) of
196− [fi] -> fn_params (snd fi)
197− [] -> []
198− xs -> error ("Too much function info: " ++ show xs)
199− in nub $ paramNames args env [x | x <- [0..length args],
200− not (x `elem` ppos)]
195+ Nothing -> let ppos = case lookupCtxtExact tn (idris_fninfo i) of
196+ Just fi -> fn_params fi
197+ Nothing -> []
198+ in nub $ paramNames args env [x | x <- [0..length args],
199+ not (x `elem` ppos)]
201200 ++ getFlexInType i env ps f ++
202201 getFlexInType i env ps a
203202 | otherwise = nub $ getFlexInType i env ps f ++