Improve location killing

src/Core/Context.idr

@@ -716,8 +716,8 @@ HasNames Error where
     = CantConvert fc gam <$> full gam rho <*> full gam s <*> full gam t
   full _ (CantSolveEq fc gam rho s t)
     = CantSolveEq fc gam <$> full gam rho <*> full gam s <*> full gam t
-  full gam (PatternVariableUnifies fc rho n s)
-    = PatternVariableUnifies fc <$> full gam rho <*> full gam n <*> full gam s
+  full gam (PatternVariableUnifies fc fct rho n s)
+    = PatternVariableUnifies fc fct <$> full gam rho <*> full gam n <*> full gam s
   full gam (CyclicMeta fc rho n s)
     = CyclicMeta fc <$> full gam rho <*> full gam n <*> full gam s
   full _ (WhenUnifying fc gam rho s t err)
@@ -804,8 +804,8 @@ HasNames Error where
     = CantConvert fc gam <$> resolved gam rho <*> resolved gam s <*> resolved gam t
   resolved _ (CantSolveEq fc gam rho s t)
     = CantSolveEq fc gam <$> resolved gam rho <*> resolved gam s <*> resolved gam t
-  resolved gam (PatternVariableUnifies fc rho n s)
-    = PatternVariableUnifies fc <$> resolved gam rho <*> resolved gam n <*> resolved gam s
+  resolved gam (PatternVariableUnifies fc fct rho n s)
+    = PatternVariableUnifies fc fct <$> resolved gam rho <*> resolved gam n <*> resolved gam s
   resolved gam (CyclicMeta fc rho n s)
     = CyclicMeta fc <$> resolved gam rho <*> resolved gam n <*> resolved gam s
   resolved _ (WhenUnifying fc gam rho s t err)

src/Core/Core.idr

@@ -81,7 +81,7 @@ data Error : Type where
      CantSolveEq : {vars : _} ->
                    FC -> Context -> Env Term vars -> Term vars -> Term vars -> Error
      PatternVariableUnifies : {vars : _} ->
-                              FC -> Env Term vars -> Name -> Term vars -> Error
+                              FC -> FC -> Env Term vars -> Name -> Term vars -> Error
      CyclicMeta : {vars : _} ->
                   FC -> Env Term vars -> Name -> Term vars -> Error
      WhenUnifying : {vars : _} ->
@@ -207,7 +207,7 @@ Show Error where
       = show fc ++ ":Type mismatch: " ++ show x ++ " and " ++ show y
   show (CantSolveEq fc _ env x y)
       = show fc ++ ":" ++ show x ++ " and " ++ show y ++ " are not equal"
-  show (PatternVariableUnifies fc env n x)
+  show (PatternVariableUnifies fc fct env n x)
       = show fc ++ ":Pattern variable " ++ show n ++ " unifies with " ++ show x
   show (CyclicMeta fc env n tm)
       = show fc ++ ":Cycle detected in metavariable solution " ++ show n
@@ -390,7 +390,7 @@ getErrorLoc : Error -> Maybe FC
 getErrorLoc (Fatal err) = getErrorLoc err
 getErrorLoc (CantConvert loc _ _ _ _) = Just loc
 getErrorLoc (CantSolveEq loc _ _ _ _) = Just loc
-getErrorLoc (PatternVariableUnifies loc _ _ _) = Just loc
+getErrorLoc (PatternVariableUnifies loc _ _ _ _) = Just loc
 getErrorLoc (CyclicMeta loc _ _ _) = Just loc
 getErrorLoc (WhenUnifying loc _ _ _ _ _) = Just loc
 getErrorLoc (ValidCase loc _ _) = Just loc
@@ -466,7 +466,7 @@ killWarningLoc : Warning -> Warning
 killWarningLoc (ParserWarning fc x) = ParserWarning emptyFC x
 killWarningLoc (UnreachableClause fc x y) = UnreachableClause emptyFC x y
 killWarningLoc (ShadowingGlobalDefs fc xs) = ShadowingGlobalDefs emptyFC xs
-killWarningLoc (Deprecated x y) = Deprecated x y
+killWarningLoc (Deprecated x y) = Deprecated x (map ((emptyFC,) . snd) y)
 killWarningLoc (GenericWarn x) = GenericWarn x
 
 export
@@ -474,7 +474,7 @@ killErrorLoc : Error -> Error
 killErrorLoc (Fatal err) = Fatal (killErrorLoc err)
 killErrorLoc (CantConvert fc x y z w) = CantConvert emptyFC x y z w
 killErrorLoc (CantSolveEq fc x y z w) = CantSolveEq emptyFC x y z w
-killErrorLoc (PatternVariableUnifies fc x y z) = PatternVariableUnifies emptyFC x y z
+killErrorLoc (PatternVariableUnifies fc fct x y z) = PatternVariableUnifies emptyFC emptyFC x y z
 killErrorLoc (CyclicMeta fc x y z) = CyclicMeta emptyFC x y z
 killErrorLoc (WhenUnifying fc x y z w err) = WhenUnifying emptyFC x y z w (killErrorLoc err)
 killErrorLoc (ValidCase fc x y) = ValidCase emptyFC x y
@@ -525,7 +525,7 @@ killErrorLoc (FileErr x y) = FileErr x y
 killErrorLoc (CantFindPackage x) = CantFindPackage x
 killErrorLoc (LitFail fc) = LitFail emptyFC
 killErrorLoc (LexFail fc x) = LexFail emptyFC x
-killErrorLoc (ParseFail xs) = ParseFail xs
+killErrorLoc (ParseFail xs) = ParseFail $ map ((emptyFC,) . snd) $ xs
 killErrorLoc (ModuleNotFound fc x) = ModuleNotFound emptyFC x
 killErrorLoc (CyclicImports xs) = CyclicImports xs
 killErrorLoc ForceNeeded = ForceNeeded

src/Core/Unify.idr

@@ -463,7 +463,7 @@ tryInstantiate {newvars} loc mode env mname mref num mdef locs otm tm
 --          let Hole _ _ = definition mdef
 --              | def => ufail {a=()} loc (show mname ++ " already resolved as " ++ show def)
          case fullname mdef of
-              PV pv pi => throw (PatternVariableUnifies loc env (PV pv pi) otm)
+              PV pv pi => throw (PatternVariableUnifies loc (getLoc otm) env (PV pv pi) otm)
               _ => pure ()
          defs <- get Ctxt
          ty <- normalisePis defs [] $ type mdef

src/Idris/Error.idr

@@ -60,7 +60,7 @@ Eq Error where
   Fatal err1 == Fatal err2 = err1 == err2
   CantConvert fc1 gam1 rho1 s1 t1 == CantConvert fc2 gam2 rho2 s2 t2 = fc1 == fc2
   CantSolveEq fc1 gam1 rho s1 t1 == CantSolveEq fc2 gam2 rho2 s2 t2 = fc1 == fc2
-  PatternVariableUnifies fc1 rho1 n1 s1 == PatternVariableUnifies fc2 rho2 n2 s2 = fc1 == fc2 && n1 == n2
+  PatternVariableUnifies fc1 fct1 rho1 n1 s1 == PatternVariableUnifies fc2 fct2 rho2 n2 s2 = fc1 == fc2 && fct1 == fct2 && n1 == n2
   CyclicMeta fc1 rho1 n1 s1 == CyclicMeta fc2 rho2 n2 s2 = fc1 == fc2 && n1 == n2
   WhenUnifying fc1 gam1 rho1 s1 t1 err1 == WhenUnifying fc2 gam2 rho2 s2 t2 err2 = fc1 == fc2 && err1 == err2
   ValidCase fc1 rho1 x1 == ValidCase fc2 rho2 x2 = fc1 == fc2
@@ -313,8 +313,8 @@ perrorRaw (CantSolveEq fc gam env l r)
                       ]) <+> line <+> !(ploc fc)
          put Ctxt defs
          pure res
-perrorRaw (PatternVariableUnifies fc env n tm)
-    = do let (min, max) = order fc (getLoc tm)
+perrorRaw (PatternVariableUnifies fc fct env n tm)
+    = do let (min, max) = order fc fct
          pure $ errorDesc (hsep [ reflow "Pattern variable"
                   , code (prettyVar n)
                   , reflow "unifies with" <+> colon