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

@@ -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

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)
 

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.