From 7e5ddafc4ddcd1baddf2b80b9395d9281251da6a Mon Sep 17 00:00:00 2001 From: Viktor Yudov Date: Fri, 20 Dec 2024 15:28:58 +0300 Subject: [PATCH 1/2] [ fix ] Fix `%search` in constraint --- src/Idris/Elab/Interface.idr | 34 ++++++++++--------- .../interface/interface034/Issue3448.idr | 4 +++ tests/idris2/interface/interface034/expected | 1 + tests/idris2/interface/interface034/run | 3 ++ 4 files changed, 26 insertions(+), 16 deletions(-) create mode 100644 tests/idris2/interface/interface034/Issue3448.idr create mode 100644 tests/idris2/interface/interface034/expected create mode 100644 tests/idris2/interface/interface034/run diff --git a/src/Idris/Elab/Interface.idr b/src/Idris/Elab/Interface.idr index f0835b4247..7c4ae32a93 100644 --- a/src/Idris/Elab/Interface.idr +++ b/src/Idris/Elab/Interface.idr @@ -97,6 +97,15 @@ mkDataTy fc [] = IType fc mkDataTy fc ((n, (_, ty)) :: ps) = IPi fc top Explicit (Just n) ty (mkDataTy fc ps) +jname : (Name, (RigCount, RawImp)) -> (Maybe Name, RigCount, RawImp) +jname (n, rig, t) = (Just n, rig, t) + +mkTy : FC -> PiInfo RawImp -> + List (Maybe Name, RigCount, RawImp) -> RawImp -> RawImp +mkTy fc imp [] ret = ret +mkTy fc imp ((n, c, argty) :: args) ret + = IPi fc c imp n argty (mkTy fc imp args ret) + mkIfaceData : {vars : _} -> {auto c : Ref Ctxt Defs} -> FC -> WithDefault Visibility Private -> Env Term vars -> @@ -109,8 +118,9 @@ mkIfaceData {vars} ifc def_vis env constraints n conName ps dets meths else [NoHints, UniqueSearch, SearchBy dets] pNames = map fst ps retty = apply (IVar vfc n) (map (IVar EmptyFC) pNames) - conty = mkTy Implicit (map jname ps) $ - mkTy AutoImplicit (map bhere constraints) (mkTy Explicit (map bname meths) retty) + conty = mkTy vfc Implicit (map jname ps) $ + mkTy vfc AutoImplicit (map bhere constraints) $ + mkTy vfc Explicit (map bname meths) retty con = MkImpTy vfc (NoFC conName) !(bindTypeNames ifc [] (pNames ++ map fst meths ++ vars) conty) bound = pNames ++ map fst meths ++ vars in @@ -119,25 +129,15 @@ mkIfaceData {vars} ifc def_vis env constraints n conName ps dets meths (Just !(bindTypeNames ifc [] bound (mkDataTy vfc ps))) opts [con] where - vfc : FC vfc = virtualiseFC ifc - jname : (Name, (RigCount, RawImp)) -> (Maybe Name, RigCount, RawImp) - jname (n, rig, t) = (Just n, rig, t) - bname : (Name, RigCount, RawImp) -> (Maybe Name, RigCount, RawImp) bname (n, c, t) = (Just n, c, IBindHere (getFC t) (PI erased) t) bhere : (Maybe Name, RigCount, RawImp) -> (Maybe Name, RigCount, RawImp) bhere (n, c, t) = (n, c, IBindHere (getFC t) (PI erased) t) - mkTy : PiInfo RawImp -> - List (Maybe Name, RigCount, RawImp) -> RawImp -> RawImp - mkTy imp [] ret = ret - mkTy imp ((n, c, argty) :: args) ret - = IPi vfc c imp n argty (mkTy imp args ret) - -- Get the implicit arguments for a method declaration or constraint hint -- to allow us to build the data declaration getMethDecl : {vars : _} -> @@ -246,11 +246,13 @@ getConstraintHint : {vars : _} -> Name -> Name -> (constraints : List Name) -> (allmeths : List Name) -> - (params : List Name) -> + (params : List (Name, RigCount, RawImp)) -> (Name, RawImp) -> Core (Name, List ImpDecl) getConstraintHint {vars} fc env vis iname cname constraints meths params (cn, con) - = do let ity = apply (IVar fc iname) (map (IVar fc) params) - let fty = IPi fc top Explicit Nothing ity con + = do let pNames = map fst params + let ity = apply (IVar fc iname) (map (IVar fc) pNames) + let fty = mkTy fc Implicit (map jname params) $ + mkTy fc Explicit [(Nothing, top, ity)] con ty_imp <- bindTypeNames fc [] (meths ++ vars) fty let hintname = DN ("Constraint " ++ show con) (UN (Basic $ "__" ++ show iname ++ "_" ++ show con)) @@ -521,7 +523,7 @@ elabInterface {vars} ifc def_vis env nest constraints iname params dets mcon bod iname conName (map fst nconstraints) meth_names - paramNames) nconstraints + params) nconstraints log "elab.interface" 5 $ "Constraint hints from " ++ show constraints ++ ": " ++ show chints traverse_ (processDecl [] nest env) (concatMap snd chints) traverse_ (\n => do mn <- inCurrentNS n diff --git a/tests/idris2/interface/interface034/Issue3448.idr b/tests/idris2/interface/interface034/Issue3448.idr new file mode 100644 index 0000000000..6b393fd3bf --- /dev/null +++ b/tests/idris2/interface/interface034/Issue3448.idr @@ -0,0 +1,4 @@ +X : Type +data Y : X -> Type + +interface Y %search => Z (x : X) where diff --git a/tests/idris2/interface/interface034/expected b/tests/idris2/interface/interface034/expected new file mode 100644 index 0000000000..784ac57ef4 --- /dev/null +++ b/tests/idris2/interface/interface034/expected @@ -0,0 +1 @@ +1/1: Building Issue3448 (Issue3448.idr) diff --git a/tests/idris2/interface/interface034/run b/tests/idris2/interface/interface034/run new file mode 100644 index 0000000000..fe690174dc --- /dev/null +++ b/tests/idris2/interface/interface034/run @@ -0,0 +1,3 @@ +. ../../../testutils.sh + +check Issue3448.idr From 1cdef0ac5a27f8ef9dab7bb6f53bbd5c4ed136c4 Mon Sep 17 00:00:00 2001 From: Viktor Yudov Date: Fri, 20 Dec 2024 16:14:29 +0300 Subject: [PATCH 2/2] [ test ] Update `expected` in `basic049` --- tests/idris2/basic/basic049/expected | 24 ------------------------ 1 file changed, 24 deletions(-) diff --git a/tests/idris2/basic/basic049/expected b/tests/idris2/basic/basic049/expected index 8845b447d8..fc710934f3 100644 --- a/tests/idris2/basic/basic049/expected +++ b/tests/idris2/basic/basic049/expected @@ -15,30 +15,6 @@ Warning: We are about to implicitly bind the following lowercase names. You may be unintentionally shadowing the associated global definitions: a is shadowing Main.R2.R2.a, Main.R1.R1.a -Fld:76:1--81:38 - 76 | interface Show a => (num : Num a) => MyIface a where -- Some interface with - 77 | constructor MkIface - 78 | -- constraints - 79 | data MyData : a -> Type -- and a data declaration. - 80 | someFunc : a -> a -- Constraints are now elaborated as auto implicits (as one would expect) - 81 | giveBack : {x : a} -> MyData x -> a -- (previously as explicit arguments of the interface - -Warning: We are about to implicitly bind the following lowercase names. -You may be unintentionally shadowing the associated global definitions: - a is shadowing Main.R2.R2.a, Main.R1.R1.a - -Fld:76:1--81:38 - 76 | interface Show a => (num : Num a) => MyIface a where -- Some interface with - 77 | constructor MkIface - 78 | -- constraints - 79 | data MyData : a -> Type -- and a data declaration. - 80 | someFunc : a -> a -- Constraints are now elaborated as auto implicits (as one would expect) - 81 | giveBack : {x : a} -> MyData x -> a -- (previously as explicit arguments of the interface - -Warning: We are about to implicitly bind the following lowercase names. -You may be unintentionally shadowing the associated global definitions: - a is shadowing Main.R2.R2.a, Main.R1.R1.a - Fld:86:3--86:37 82 | -- constructor) 83 |