Add test for eta

src/Core/UnifyState.idr

@@ -524,7 +524,8 @@ checkValidHole (idx, (fc, n))
                                 ynf <- normaliseHoles defs env y
                                 throw (CantSolveEq fc env xnf ynf)
                           _ => pure ()
-              _ => traverse_ checkRef (keys (getRefs (Resolved (-1)) (type gdef)))
+              _ => traverse_ checkRef !(traverse getFullName
+                                        ((keys (getRefs (Resolved (-1)) (type gdef)))))
   where
     checkRef : Name -> Core ()
     checkRef (PV n f)

src/Idris/Error.idr

@@ -40,8 +40,12 @@ perror (CantSolveEq _ env l r)
     = pure $ "Can't solve constraint between:\n\t" ++ !(pshow env l) ++ 
       "\nand\n\t" ++ !(pshow env r)
 perror (PatternVariableUnifies _ env n tm)
-    = pure $ "Pattern variable " ++ show n ++ 
-      "unifies with:\n\t" ++ !(pshow env tm)
+    = pure $ "Pattern variable " ++ showPVar n ++ 
+      " unifies with:\n\t" ++ !(pshow env tm)
+  where
+    showPVar : Name -> String
+    showPVar (PV n _) = showPVar n
+    showPVar n = show n
 perror (CyclicMeta _ n)
     = pure $ "Cycle detected in solution of metavariable " ++ show n
 perror (WhenUnifying _ env x y err)

src/TTImp/BindImplicits.idr

@@ -51,7 +51,12 @@ renameIBinds rs us (IDelay fc t)
 renameIBinds rs us (IForce fc t)
     = pure $ IForce fc !(renameIBinds rs us t)
 renameIBinds rs us (IAlternative fc u alts)
-    = pure $ IAlternative fc u !(traverse (renameIBinds rs us) alts)
+    = pure $ IAlternative fc !(renameAlt u)
+                             !(traverse (renameIBinds rs us) alts)
+  where
+    renameAlt : AltType -> State (List (String, String)) AltType
+    renameAlt (UniqueDefault t) = pure $ UniqueDefault !(renameIBinds rs us t)
+    renameAlt u = pure u
 renameIBinds rs us (IBindVar fc n)
     = if n `elem` rs
          then do let n' = getUnique (rs ++ us) n
@@ -93,7 +98,11 @@ doBind ns (IDelay fc tm)
 doBind ns (IForce fc tm)
     = IForce fc (doBind ns tm)
 doBind ns (IAlternative fc u alts)
-    = IAlternative fc u (map (doBind ns) alts)
+    = IAlternative fc (doBindAlt u) (map (doBind ns) alts)
+  where
+    doBindAlt : AltType -> AltType
+    doBindAlt (UniqueDefault t) = UniqueDefault (doBind ns t)
+    doBindAlt u = u
 doBind ns tm = tm
 
 export

src/TTImp/ProcessDef.idr

@@ -592,6 +592,8 @@ processDef opts nest env fc n_in cs_in
 
          let rmetas = getMetas tree_ct
          traverse_ addToSave (keys rmetas)
+         let tymetas = getMetas (type gdef)
+         traverse_ addToSave (keys tymetas)
          addToSave n
          log 10 $ "Saving from " ++ show n ++ ": " ++ show (keys rmetas)
 

tests/Main.idr

@@ -26,6 +26,7 @@ idrisTests
     = ["basic001", "basic002", "basic003", "basic004", "basic005",
        "basic006", "basic007", "basic008", "basic009", "basic010",
        "basic011", "basic012", "basic013", "basic014", "basic015",
+       "basic016",
        "coverage001", "coverage002",
        "error001", "error002", "error003", "error004", "error005",
        "error006",

tests/idris2/basic016/Eta.idr

@@ -0,0 +1,14 @@
+data Test : Type where
+     MkTest : Integer -> Integer -> Test
+
+etaGood1 : MkTest = (\x => \y => MkTest ? ?)
+etaGood1 = Refl
+
+etaGood2: (MkTest 1) = (\x => MkTest ? x)
+etaGood2 = Refl
+
+etaGood3: (f : a -> b) -> f = (\x => f x)
+etaGood3 f = Refl
+
+etaBad : MkTest = (\x : Nat => \y => MkTest ? ?)
+etaBad = Refl

tests/idris2/basic016/Eta2.idr

@@ -0,0 +1,5 @@
+test : Builtin.Equal S (\x : a => S ?)
+test = Refl
+
+test2 : ?
+test2 = {a : _} -> the (S = \x : a => S _) Refl

tests/idris2/basic016/expected

@@ -0,0 +1,20 @@
+1/1: Building Eta (Eta.idr)
+Eta.idr:14:10--15:1:While processing right hand side of Main.etaBad at Eta.idr:14:1--15:1:
+When unifying ?x = ?x and MkTest = (\x => (\y => (MkTest ?_ ?_)))
+Mismatch between:
+	Integer
+and
+	Nat
+1/1: Building Eta2 (Eta2.idr)
+Eta2.idr:2:8--4:1:While processing right hand side of Main.test at Eta2.idr:2:1--4:1:
+When unifying ?x = ?x and S = (\x => (S ?_))
+Mismatch between:
+	Nat
+and
+	a
+Eta2.idr:5:44--6:1:While processing right hand side of Main.test2 at Eta2.idr:5:1--6:1:
+When unifying ?x = ?x and S = (\x => (S ?_))
+Mismatch between:
+	Nat
+and
+	a

tests/idris2/basic016/run

@@ -0,0 +1,4 @@
+$1 --check Eta.idr
+$1 --check Eta2.idr
+
+rm -rf build