@@ -572,11 +572,12 @@ prepare_apply fn imps =
572 env <- get_env
572 env <- get_env
573 -- let claims = getArgs ty imps
573 -- let claims = getArgs ty imps
574 -- claims <- mkClaims (normalise ctxt env ty) imps []
574 -- 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
578+ else normalise ctxt env (finalise ty)
575 claims <- -- trace (show (fn, imps, ty, map fst env, normalise ctxt env (finalise ty))) $
579 claims <- -- trace (show (fn, imps, ty, map fst env, normalise ctxt env (finalise ty))) $
576− mkClaims (finalise ty)
577− (normalise ctxt env (finalise ty))
579− imps [] (map fst env)
580+ mkClaims usety imps [] (map fst env)
580 ES (p, a) s prev <- get
581 ES (p, a) s prev <- get
581 -- reverse the claims we made so that args go left to right
582 -- reverse the claims we made so that args go left to right
582 let n = length (filter not imps)
583 let n = length (filter not imps)
@@ -584,14 +585,17 @@ prepare_apply fn imps =
584 put (ES (p { holes = h : (reverse (take n hs) ++ drop n hs) }, a) s prev)
585 put (ES (p { holes = h : (reverse (take n hs) ++ drop n hs) }, a) s prev)
585 return $! claims
586 return $! claims
588+ argsOK :: Type -> [a] -> Bool
589+ argsOK (Bind n (Pi _ _ _) sc) (i : is) = argsOK sc is
590+ argsOK _ (i : is) = False
587 mkClaims :: Type -- ^ The type of the operation being applied
593 mkClaims :: Type -- ^ The type of the operation being applied
588− -> Type -- ^ Normalised version if we need it
589− -> Bool -- ^ Using normalised verison
590 -> [Bool] -- ^ Whether the arguments are implicit
594 -> [Bool] -- ^ Whether the arguments are implicit
591 -> [(Name, Name)] -- ^ Accumulator for produced claims
595 -> [(Name, Name)] -- ^ Accumulator for produced claims
592 -> [Name] -- ^ Hypotheses
596 -> [Name] -- ^ Hypotheses
593 -> Elab' aux [(Name, Name)] -- ^ The names of the arguments and their holes, resp.
597 -> 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 =
595 do let t = rebind hs t_in
599 do let t = rebind hs t_in
596 n <- getNameFrom (mkMN n')
600 n <- getNameFrom (mkMN n')
597-- when (null claims) (start_unify n)
601-- when (null claims) (start_unify n)
@@ -599,12 +603,9 @@ prepare_apply fn imps =
599 env <- get_env
603 env <- get_env
600 claim n (forgetEnv (map fst env) t)
604 claim n (forgetEnv (map fst env) t)
601 when i (movelast n)
605 when i (movelast n)
602− mkClaims sc' scn norm is ((n', n) : claims) hs
606+ mkClaims sc' 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 t [] claims _ = return $! (reverse claims)
607− mkClaims _ _ _ _ _ _
608+ mkClaims _ _ _ _
608 | Var n <- fn
609 | Var n <- fn
609 = do ctxt <- get_context
610 = do ctxt <- get_context
610 case lookupTy n ctxt of
611 case lookupTy n ctxt of