Convert to full names before computing hashes.

src/Core/Context.idr

@@ -885,6 +885,9 @@ clearCtxt
     resetElab : Options -> Options
     resetElab = record { elabDirectives = defaultElab }
 
+-- Beware: if your hashable thing contains (potentially resolved) names,
+-- it'll be better to use addHashWithNames to make the hash independent
+-- of the internal numbering of names.
 export
 addHash : {auto c : Ref Ctxt Defs} ->
           Hashable a => a -> Core ()
@@ -1181,6 +1184,15 @@ prettyName (WithBlock outer idx)
 prettyName (NS ns n) = prettyName n
 prettyName n = pure (show n)
 
+-- Add a hash of a thing that contains names,
+-- but convert the internal numbers to full numbers first.
+-- This makes the hash not depend on the internal numbering,
+-- which is unstable.
+export
+addHashWithNames : {auto c : Ref Ctxt Defs} ->
+  Hashable a => HasNames a => a -> Core ()
+addHashWithNames x = toFullNames x >>= addHash
+
 export
 setFlag : {auto c : Ref Ctxt Defs} ->
         FC -> Name -> DefFlag -> Core ()

src/TTImp/ProcessData.idr

@@ -107,8 +107,8 @@ checkCon {vars} opts nest env vis tn_in tn (MkImpTy fc cn_in ty_raw)
          log 10 $ "Saving from " ++ show cn ++ ": " ++ show (keys (getMetas ty))
 
          case vis of
-              Public => do addHash cn
+              Public => do addHashWithNames cn
-                           addHash fullty
+                           addHashWithNames fullty
               _ => pure ()
          pure (MkCon fc cn !(getArity defs [] fullty) fullty)
 
@@ -278,8 +278,8 @@ processData {vars} eopts nest env fc vis (MkImpLater dfc n_in ty_raw)
 
          case vis of
               Private => pure ()
-              _ => do addHash n
+              _ => do addHashWithNames n
-                      addHash fullty
+                      addHashWithNames fullty
          pure ()
 
 processData {vars} eopts nest env fc vis (MkImpData dfc n_in ty_raw opts cons_raw)
@@ -323,8 +323,8 @@ processData {vars} eopts nest env fc vis (MkImpData dfc n_in ty_raw opts cons_ra
                           (TCon 0 arity [] [] defaultFlags [] [] Nothing))
          case vis of
               Private => pure ()
-              _ => do addHash n
+              _ => do addHashWithNames n
-                      addHash fullty
+                      addHashWithNames fullty
 
          -- Constructors are private if the data type as a whole is
          -- export

src/TTImp/ProcessDef.idr

@@ -393,8 +393,8 @@ checkClause {vars} mult hashit n opts nest env (PatClause fc lhs_in rhs)
 
          logTerm 3 "RHS term" rhstm
          when hashit $
-           do addHash lhstm'
+           do addHashWithNames lhstm'
-              addHash rhstm
+              addHashWithNames rhstm
 
          -- If the rhs is a hole, record the lhs in the metadata because we
          -- might want to split it interactively

src/TTImp/ProcessType.idr

@@ -301,5 +301,5 @@ processType {vars} eopts nest env fc rig vis opts (MkImpTy tfc n_in ty_raw)
          log 10 $ "Saving from " ++ show n ++ ": " ++ show (keys (getMetas ty))
 
          when (vis /= Private) $
-              do addHash n
+              do addHashWithNames n
-                 addHash ty
+                 addHashWithNames ty