Unbound implicits are invertible in terms

Just like all other pi-bound things, if m is an unbound implicit and we have m ?x = m y as a unification problem, we can conclude ?x = y because it has to be true for all ms. This was implemented in Blodwen but I hadn't got around to it yet for Idris2... fortunately it's a bit easier in Idris2! Fixes idris-lang#44
melted · Jul 26, 2019 · 8e9655d · 8e9655d
1 parent 4f4d4cc
commit 8e9655d
Show file tree

Hide file tree

Showing 9 changed files with 41 additions and 28 deletions.
diff --git a/src/Core/AutoSearch.idr b/src/Core/AutoSearch.idr
@@ -45,7 +45,7 @@ mkArgs fc rigc env (NBind nfc x (Pi c p ty) sc)
          let argRig = rigMult rigc c
          (idx, arg) <- newMeta fc argRig env nm argTy 
                                (Hole (length env) False) False
-         setInvertible fc idx
+         setInvertible fc (Resolved idx)
          (rest, restTy) <- mkArgs fc rigc env 
                               !(sc defs (toClosure defaultOpts env arg))
          pure (MkArgInfo idx argRig p arg argTy :: rest, restTy)

diff --git a/src/Core/Unify.idr b/src/Core/Unify.idr
@@ -556,19 +556,16 @@ mutual
       = postpone loc "Postponing hole application" env 
                  (NApp loc (NMeta mname mref margs) margs') tm
 
-  unifyPatVar : {auto c : Ref Ctxt Defs} ->
-                {auto u : Ref UST UState} ->
-                {vars : _} ->
-                UnifyMode -> FC -> Env Term vars ->
-                (metaname : Name) -> (metaref : Int) ->
-                (margs : List (Closure vars)) ->
-                (margs' : List (Closure vars)) ->
-                (soln : NF vars) ->
-                Core UnifyResult
-  -- TODO: if either side is a pattern variable application, and we're in a term,
-  -- (which will be a type) we can proceed because the pattern variable
-  -- has to end up pi bound. Unify the right most variables, and continue.
-  unifyPatVar mode loc env mname mref margs margs' tm
+  postponePatVar : {auto c : Ref Ctxt Defs} ->
+                   {auto u : Ref UST UState} ->
+                   {vars : _} ->
+                   UnifyMode -> FC -> Env Term vars ->
+                   (metaname : Name) -> (metaref : Int) ->
+                   (margs : List (Closure vars)) ->
+                   (margs' : List (Closure vars)) ->
+                   (soln : NF vars) ->
+                   Core UnifyResult
+  postponePatVar mode loc env mname mref margs margs' tm
       = postpone loc "Not in pattern fragment" env 
                  (NApp loc (NMeta mname mref margs) margs') tm
 
@@ -630,12 +627,12 @@ mutual
            case !(patternEnv env args) of
                 Nothing => 
                   do Just hdef <- lookupCtxtExact (Resolved mref) (gamma defs)
-                        | _ => unifyPatVar mode loc env mname mref margs margs' tmnf
+                        | _ => postponePatVar mode loc env mname mref margs margs' tmnf
                      let Hole _ _ = definition hdef
-                        | _ => unifyPatVar mode loc env mname mref margs margs' tmnf
+                        | _ => postponePatVar mode loc env mname mref margs margs' tmnf
                      if invertible hdef
                         then unifyHoleApp mode loc env mname mref margs margs' tmnf
-                        else unifyPatVar mode loc env mname mref margs margs' tmnf
+                        else postponePatVar mode loc env mname mref margs margs' tmnf
                 Just (newvars ** (locs, submv)) => 
                   do tm <- quote empty env tmnf
                      case shrinkTerm tm submv of
@@ -1015,12 +1012,12 @@ mutual
 
 export
 setInvertible : {auto c : Ref Ctxt Defs} ->
-                FC -> Int -> Core ()
-setInvertible loc i
+                FC -> Name -> Core ()
+setInvertible fc n
     = do defs <- get Ctxt
-         Just gdef <- lookupCtxtExact (Resolved i) (gamma defs)
-              | Nothing => pure ()
-         addDef (Resolved i) (record { invertible = True } gdef)
+         Just gdef <- lookupCtxtExact n (gamma defs)
+              | Nothing => throw (UndefinedName fc n)
+         addDef n (record { invertible = True } gdef)
          pure ()
 
 public export
@@ -1083,7 +1080,7 @@ retryGuess mode smode (hid, (loc, hname))
                                 DeterminingArg _ n i _ _ => 
                                     do logTerm 5 ("Failed (det " ++ show hname ++ " " ++ show n ++ ")")
                                                  (type def)
-                                       setInvertible loc i
+                                       setInvertible loc (Resolved i)
                                        pure False -- progress made!
                                 _ => do logTerm 5 ("Search failed for " ++ show hname) 
                                                   (type def)

diff --git a/src/Idris/Elab/Interface.idr b/src/Idris/Elab/Interface.idr
@@ -109,21 +109,22 @@ getMethToplevel {vars} env vis iname cname constraints allmeths params
          -- which appear in other method types
          let ty_constr = substNames vars (map applyCon allmeths) ty
          ty_imp <- bindTypeNames vars (bindIFace fc ity ty_constr)
+         cn <- inCurrentNS n
          let tydecl = IClaim fc c vis (if d then [Inline, Invertible]
                                             else [Inline]) 
-                                      (MkImpTy fc n ty_imp) 
+                                      (MkImpTy fc cn ty_imp) 
          let conapp = apply (IVar fc cname)
                          (map (const (Implicit fc True)) constraints ++
                           map (IBindVar fc) (map bindName allmeths))
          let argns = getExplicitArgs 0 ty
          -- eta expand the RHS so that we put implicits in the right place
-         let fnclause = PatClause fc (IImplicitApp fc (IVar fc n) 
+         let fnclause = PatClause fc (IImplicitApp fc (IVar fc cn) 
                                                    (Just (UN "__con"))
                                                    conapp)
                                   (mkLam argns 
                                     (apply (IVar fc (methName n))
                                            (map (IVar fc) argns)))
-         let fndef = IDef fc n [fnclause]
+         let fndef = IDef fc cn [fnclause]
          pure [tydecl, fndef]
   where
     applyCon : Name -> (Name, RawImp)

diff --git a/src/TTImp/Elab/ImplicitBind.idr b/src/TTImp/Elab/ImplicitBind.idr
@@ -430,6 +430,10 @@ checkBindVar rig elabinfo nest env fc str topexp
                 do (tm, exp, bty) <- mkPatternHole fc rig n env
                                               (implicitMode elabinfo)
                                               topexp
+                   -- In PI mode, it's invertible like any other pi bound thing
+                   case implicitMode elabinfo of
+                        PI _ => setInvertible fc n
+                        _ => pure ()
                    log 5 $ "Added Bound implicit " ++ show (n, (rig, tm, exp, bty))
                    defs <- get Ctxt
                    est <- get EST

diff --git a/src/TTImp/ProcessType.idr b/src/TTImp/ProcessType.idr
@@ -74,7 +74,7 @@ processType {vars} eopts nest env fc rig vis opts (MkImpTy tfc n_in ty_raw)
                    checkTerm idx InType (HolesOkay :: eopts) nest env 
                              (IBindHere fc (PI Rig0) ty_raw) 
                              (gType fc)
-         logTermNF 5 (show n) [] (abstractEnvType tfc env ty)
+         logTermNF 5 ("Type of " ++ show n) [] (abstractEnvType tfc env ty)
          -- TODO: Check name visibility
          -- If it's declared as externally defined, set the definition to
          -- ExternFn <arity>, where the arity is assumed to be fixed (i.e.

diff --git a/tests/Main.idr b/tests/Main.idr
@@ -38,7 +38,7 @@ idrisTests
        "interactive009", "interactive010", "interactive011", "interactive012",
        "interface001", "interface002", "interface003", "interface004",
        "interface005", "interface006", "interface007", "interface008",
-       "interface009",
+       "interface009", "interface010",
        "lazy001",
        "linear001", "linear002", "linear003", "linear004", "linear005",
        "linear006", "linear007",

diff --git a/tests/idris2/interface010/Dep.idr b/tests/idris2/interface010/Dep.idr
@@ -0,0 +1,7 @@
+module Dep
+
+interface Monad m => FooBar m where
+  Foo : {0 a : Type} -> a -> m a -> Type
+  Bar : {0 A : Type} -> m A -> Type
+  foo : {0 A : Type} -> (x : A) -> (ma : m A) -> Foo x ma -> Bar ma
+
diff --git a/tests/idris2/interface010/expected b/tests/idris2/interface010/expected
@@ -0,0 +1 @@
+1/1: Building Dep (Dep.idr)
diff --git a/tests/idris2/interface010/run b/tests/idris2/interface010/run
@@ -0,0 +1,3 @@
+$1 Dep.idr --check
+
+rm -rf build