Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[ fix #3448 ] Fix %search in constraint #3451

Open
wants to merge 2 commits into
base: main
Choose a base branch
from
Open

[ fix #3448 ] Fix %search in constraint #3451

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
7e5ddaf
[ fix ] Fix `%search` in constraint
spcfox Dec 20, 2024
1cdef0a
[ test ] Update `expected` in `basic049`
spcfox Dec 20, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
34 changes: 18 additions & 16 deletions src/Idris/Elab/Interface.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 ->
Expand All @@ -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

Expand All @@ -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 : _} ->
Expand Down Expand Up @@ -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
Copy link
Contributor Author

@spcfox spcfox Dec 20, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Do I need to add parameters?

ty_imp <- bindTypeNames fc [] (pNames ++ meths ++ vars) fty

like in mkIfaceData

Idris2/src/Idris/Elab/Interface.idr

Line 114 in 457ca7c

con = MkImpTy vfc (NoFC conName) !(bindTypeNames ifc [] (pNames ++ map fst meths ++ vars) conty)

and in getMethDecl

Idris2/src/Idris/Elab/Interface.idr

Line 152 in 457ca7c

ty_imp <- bindTypeNames EmptyFC [] (paramNames ++ mnames ++ vars) ty

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It seems to me that this might be necessary since I added parameters to fty, but I can't think of an example where this would have an impact

let hintname = DN ("Constraint " ++ show con)
(UN (Basic $ "__" ++ show iname ++ "_" ++ show con))
Expand Down Expand Up @@ -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
Expand Down
24 changes: 0 additions & 24 deletions tests/idris2/basic/basic049/expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Comment on lines -18 to -41
Copy link
Contributor Author

@spcfox spcfox Dec 20, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It looks like these warnings were occurring in hints for constraints. They disappeared after changes to getConstraintHint. I'm not sure if they are useful, but it seems odd

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not sure if they are useful, but it seems odd

To me these warning look completely okay, since both interface definition and interface implementations seem to shadow the top-level as

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, but in the following code MyIface0, MyIface1 and MyIface2 produce 0, 1 and 2 warnings respectively. This means that one warning per constraint is generated. This is because they do not arise from the data the interface is elabored into, but from the constraint hint. This is strange

a : Type

interface MyIface0 a where
  f0 : a -> Type

interface Show a => MyIface1 a where
  f1 : a -> Type

interface Show a => (num : Num a) => MyIface2 a where
  f2 : a -> Type

Copy link
Contributor Author

@spcfox spcfox Dec 22, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

A warning about shadowing is produced when a is an unbound implicit, but in the above examples a is explicitly bound

a : Type

-- Produce warning
interface Iface1 (x : a) where

-- No warning
interface Iface2 a (x : a) where

Previously, it was unbound at elaboration constraint hint

Fld:86:3--86:37
82 | -- constructor)
83 |
Expand Down
4 changes: 4 additions & 0 deletions tests/idris2/interface/interface034/Issue3448.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
X : Type
data Y : X -> Type

interface Y %search => Z (x : X) where
1 change: 1 addition & 0 deletions tests/idris2/interface/interface034/expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
1/1: Building Issue3448 (Issue3448.idr)
3 changes: 3 additions & 0 deletions tests/idris2/interface/interface034/run
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
. ../../../testutils.sh

check Issue3448.idr
Loading