From c65285a1f6494719a11ebd12cf8941959b77018c Mon Sep 17 00:00:00 2001
From: Edwin Brady <ecb10@st-andrews.ac.uk>
Date: Sat, 25 May 2019 20:18:43 +0100
Subject: [PATCH] Check pattern variables don't unify with things

This is bad because it means a pattern variable isn't actually a
variable, but rather has a specific value!
---
 src/Core/Core.idr             | 4 ++++
 src/Core/Unify.idr            | 9 ++++++++-
 tests/ttimp/qtt003/QTTEq.yaff | 2 +-
 3 files changed, 13 insertions(+), 2 deletions(-)

diff --git a/src/Core/Core.idr b/src/Core/Core.idr
index 0415431..88dcc1c 100644
--- a/src/Core/Core.idr
+++ b/src/Core/Core.idr
@@ -29,6 +29,7 @@ data Error
     = Fatal Error -- flag as unrecoverable (so don't postpone awaiting further info)
     | CantConvert FC (Env Term vars) (Term vars) (Term vars)
     | CantSolveEq FC (Env Term vars) (Term vars) (Term vars)
+    | PatternVariableUnifies FC (Env Term vars) Name (Term vars)
     | CyclicMeta FC Name
     | WhenUnifying FC (Env Term vars) (Term vars) (Term vars) Error
     | ValidCase FC (Env Term vars) (Either (Term vars) Error)
@@ -99,6 +100,8 @@ 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 fc ++ ":Pattern variable " ++ show n ++ " unifies with " ++ show x
   show (CyclicMeta fc n) 
       = show fc ++ ":Cycle detected in metavariable solution " ++ show n
   show (WhenUnifying fc _ x y err)
@@ -240,6 +243,7 @@ getErrorLoc : Error -> Maybe FC
 getErrorLoc (Fatal err) = getErrorLoc err
 getErrorLoc (CantConvert loc env tm y) = Just loc
 getErrorLoc (CantSolveEq loc env tm y) = Just loc
+getErrorLoc (PatternVariableUnifies loc env n x) = Just loc
 getErrorLoc (CyclicMeta loc n) = Just loc
 getErrorLoc (WhenUnifying loc env tm y z) = Just loc
 getErrorLoc (ValidCase loc env y) = Just loc
diff --git a/src/Core/Unify.idr b/src/Core/Unify.idr
index b8f748d..23d237d 100644
--- a/src/Core/Unify.idr
+++ b/src/Core/Unify.idr
@@ -307,6 +307,9 @@ instantiate {newvars} loc env mname mref mdef locs otm tm
     = do log 5 $ "Instantiating " ++ show tm ++ " in " ++ show newvars 
          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)
+              _ => pure ()
          let ty = type mdef
          defs <- get Ctxt
          rhs <- mkDef [] newvars (snocList newvars) CompatPre
@@ -556,11 +559,15 @@ mutual
                                -- so we can also unify the arguments.
               then unifyArgs mode loc env (map snd (xargs ++ xargs'))
                                           (map snd (yargs ++ yargs'))
-              else if length xargs >= length yargs
+              else if length xargs >= length yargs && not (pv xn)
                       then unifyApp False mode loc env xfc (NMeta xn xi xargs) xargs'
                                           (NApp yfc (NMeta yn yi yargs) yargs')
                       else unifyApp False mode loc env yfc (NMeta yn yi yargs) yargs'
                                           (NApp xfc (NMeta xn xi xargs) xargs')
+    where
+      pv : Name -> Bool
+      pv (PV _ _) = True
+      pv _ = False
   doUnifyBothApps mode loc env xfc fx ax yfc fy ay
       = unifyApp False mode loc env xfc fx ax (NApp yfc fy ay)
 
diff --git a/tests/ttimp/qtt003/QTTEq.yaff b/tests/ttimp/qtt003/QTTEq.yaff
index 1c744d8..77db459 100644
--- a/tests/ttimp/qtt003/QTTEq.yaff
+++ b/tests/ttimp/qtt003/QTTEq.yaff
@@ -1,7 +1,7 @@
 data Eq : $a -> $b -> Type where
      Refl : Eq $x $x
 
-okay : {p : $a -> $b} -> (1 x : $a) -> (1 y : $a) -> (1 prf : Eq x y) -> 
+okay : {p : $a -> Type} -> (1 x : $a) -> (1 y : $a) -> (1 prf : Eq x y) -> 
        p x -> p y
 -- Should fail on the LHS, before even getting to the RHS, because
 -- after elaboration 'x' appears twice even though it is linearly bound.