@@ -572,11 +572,12 @@ prepare_apply fn imps =
572572 env <- get_env
573573 -- let claims = getArgs ty imps
574574 -- claims <- mkClaims (normalise ctxt env ty) imps []
575+ -- Count arguments to check if we need to normalise the type
576+ let usety = if argsOK (finalise ty) imps
577+ then finalise ty
578+ else normalise ctxt env (finalise ty)
575579 claims <- -- trace (show (fn, imps, ty, map fst env, normalise ctxt env (finalise ty))) $
576− mkClaims (finalise ty)
577− (normalise ctxt env (finalise ty))
578− False
579− imps [] (map fst env)
580+ mkClaims usety imps [] (map fst env)
580581 ES (p, a) s prev <- get
581582 -- reverse the claims we made so that args go left to right
582583 let n = length (filter not imps)
@@ -584,14 +585,17 @@ prepare_apply fn imps =
584585 put (ES (p { holes = h : (reverse (take n hs) ++ drop n hs) }, a) s prev)
585586 return $! claims
586587 where
588+ argsOK :: Type -> [a] -> Bool
589+ argsOK (Bind n (Pi _ _ _) sc) (i : is) = argsOK sc is
590+ argsOK _ (i : is) = False
591+ argsOK _ [] = True
592+
587593 mkClaims :: Type -- ^ The type of the operation being applied
588− -> Type -- ^ Normalised version if we need it
589− -> Bool -- ^ Using normalised verison
590594 -> [Bool] -- ^ Whether the arguments are implicit
591595 -> [(Name, Name)] -- ^ Accumulator for produced claims
592596 -> [Name] -- ^ Hypotheses
593597 -> Elab' aux [(Name, Name)] -- ^ The names of the arguments and their holes, resp.
594− mkClaims (Bind n' (Pi _ t_in _) sc) (Bind _ _ scn) norm (i : is) claims hs =
598+ mkClaims (Bind n' (Pi _ t_in _) sc) (i : is) claims hs =
595599 do let t = rebind hs t_in
596600 n <- getNameFrom (mkMN n')
597601-- when (null claims) (start_unify n)
@@ -599,12 +603,9 @@ prepare_apply fn imps =
599603 env <- get_env
600604 claim n (forgetEnv (map fst env) t)
601605 when i (movelast n)
602− mkClaims sc' scn norm is ((n', n) : claims) hs
603− -- if we run out of arguments, we need the normalised version...
604− mkClaims t tn@(Bind _ _ sc) False (i : is) cs hs
605− = mkClaims tn tn True (i : is) cs hs
606− mkClaims t _ _ [] claims _ = return $! (reverse claims)
607− mkClaims _ _ _ _ _ _
606+ mkClaims sc' is ((n', n) : claims) hs
607+ mkClaims t [] claims _ = return $! (reverse claims)
608+ mkClaims _ _ _ _
608609 | Var n <- fn
609610 = do ctxt <- get_context
610611 case lookupTy n ctxt of