diff --git a/src/Core/AutoSearch.idr b/src/Core/AutoSearch.idr index 9f709ab7bd..889b43a840 100644 --- 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 index 3be44b94bd..9f358e153e 100644 --- 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 index 536c01f282..a9f049f92c 100644 --- 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 index e5bd63b2c5..420452945a 100644 --- 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 index 36d834c51e..a0c0d2a228 100644 --- 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 , where the arity is assumed to be fixed (i.e. diff --git a/tests/Main.idr b/tests/Main.idr index d4d6d5f4d1..b30788c088 100644 --- 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 new file mode 100644 index 0000000000..1e25452af3 --- /dev/null +++ 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 new file mode 100644 index 0000000000..ac16d6bbbd --- /dev/null +++ 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 new file mode 100755 index 0000000000..cdaf385952 --- /dev/null +++ b/tests/idris2/interface010/run @@ -0,0 +1,3 @@ +$1 Dep.idr --check + +rm -rf build