@@ -213,10 +213,13 @@ mergeUserImpl x y = x
213213argTys :: IState -> PTerm -> [Maybe Name]
214214argTys ist (PRef fc hls n)
215215 = case lookupTy n (tt_ctxt ist) of
216− [ty] -> map (tyName . snd) (getArgTys ty) ++ repeat Nothing
216+ [ty] -> let ty' = normalise (tt_ctxt ist) [] ty in
217+ map (tyName . snd) (getArgTys ty') ++ repeat Nothing
217218 _ -> repeat Nothing
218219 where tyName (Bind _ (Pi _ _ _) _) = Just (sUN "->")
219− tyName t | (P _ n _, _) <- unApply t = Just n
220+ tyName t | (P _ d _, [_, ty]) <- unApply t,
221+ d == sUN "Delayed" = tyName ty
222+ | (P _ n _, _) <- unApply t = Just n
220223 | otherwise = Nothing
221224argTys _ _ = repeat Nothing
222225