From 6a60680af6ff1c4febca6fedc5e158a18eaf8bb6 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Fri, 2 Jul 2021 15:59:56 +0100 Subject: [PATCH] Don't inline holes that are user defined names We inline some holes when solving them if they pose no risk to breaking sharing, since this can speed up a few things. But if the hole was originally a user name, we might want to refer to it, and inlining it menas we can't since it won't be saved to disk. --- src/Core/Unify.idr | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/Core/Unify.idr b/src/Core/Unify.idr index fee60e692..b9a6e7930 100644 --- a/src/Core/Unify.idr +++ b/src/Core/Unify.idr @@ -475,7 +475,9 @@ instantiate {newvars} loc mode env mname mref num mdef locs otm tm rhs <- mkDef locs INil tm ty logTerm "unify.instantiate" 5 "Definition" rhs - let simpleDef = MkPMDefInfo (SolvedHole num) (isSimple rhs) False + let simpleDef = MkPMDefInfo (SolvedHole num) + (not (isUserName mname) && isSimple rhs) + False let newdef = record { definition = PMDef simpleDef [] (STerm 0 rhs) (STerm 0 rhs) [] } mdef