@@ -575,6 +575,7 @@ prepare_apply fn imps =
575575 claims <- -- trace (show (fn, imps, ty, map fst env, normalise ctxt env (finalise ty))) $
576576 mkClaims (finalise ty)
577577 (normalise ctxt env (finalise ty))
578+ False
578579 imps [] (map fst env)
579580 ES (p, a) s prev <- get
580581 -- reverse the claims we made so that args go left to right
@@ -585,11 +586,12 @@ prepare_apply fn imps =
585586 where
586587 mkClaims :: Type -- ^ The type of the operation being applied
587588 -> Type -- ^ Normalised version if we need it
589+ -> Bool -- ^ Using normalised verison
588590 -> [Bool] -- ^ Whether the arguments are implicit
589591 -> [(Name, Name)] -- ^ Accumulator for produced claims
590592 -> [Name] -- ^ Hypotheses
591593 -> Elab' aux [(Name, Name)] -- ^ The names of the arguments and their holes, resp.
592− mkClaims (Bind n' (Pi _ t_in _) sc) (Bind _ _ scn) (i : is) claims hs =
594+ mkClaims (Bind n' (Pi _ t_in _) sc) (Bind _ _ scn) norm (i : is) claims hs =
593595 do let t = rebind hs t_in
594596 n <- getNameFrom (mkMN n')
595597-- when (null claims) (start_unify n)
@@ -597,11 +599,12 @@ prepare_apply fn imps =
597599 env <- get_env
598600 claim n (forgetEnv (map fst env) t)
599601 when i (movelast n)
600− mkClaims sc' scn is ((n', n) : claims) hs
602+ mkClaims sc' scn norm is ((n', n) : claims) hs
601603 -- if we run out of arguments, we need the normalised version...
602− mkClaims t tn@(Bind _ _ sc) (i : is) cs hs = mkClaims tn tn (i : is) cs hs
603− mkClaims t _ [] claims _ = return $! (reverse claims)
604− mkClaims _ _ _ _ _
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 _ _ _ _ _ _
605608 | Var n <- fn
606609 = do ctxt <- get_context
607610 case lookupTy n ctxt of