[ fix #3448 ] Fix %search in constraint
#3451
Conversation
| = 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 |
There was a problem hiding this comment.
Do I need to add parameters?
ty_imp <- bindTypeNames fc [] (pNames ++ meths ++ vars) ftylike in mkIfaceData
Idris2/src/Idris/Elab/Interface.idr
Line 114 in 457ca7c
and in
getMethDeclIdris2/src/Idris/Elab/Interface.idr
Line 152 in 457ca7c
There was a problem hiding this comment.
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
| 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 | ||
|
|
There was a problem hiding this comment.
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
There was a problem hiding this comment.
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
There was a problem hiding this comment.
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 -> TypeThere was a problem hiding this comment.
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) wherePreviously, it was unbound at elaboration constraint hint
spcfox
changed the title
%search in constraint
|
X : Type
data Y : X -> Type
failing "While processing constructor MkZ. Can't find an implementation for X"
interface Y %search => Z (y : Y x) where
constructor MkZ
interface Y x => Z (y : Y x) where
constructor MkZ
0 getX : Z y => X
getX = %searchI expected that adding |
|
Ok, it's not a problem with interfaces X : Type
data Y : X -> Type
failing "While processing constructor MkZ. Can't find an implementation for X"
interface Y %search => Z (y : Y x) where
constructor MkZ
-- The interface is elaborated into such data
failing "While processing constructor MkZ. Can't find an implementation for X"
data Z : Y x -> Type where
MkZ : {y : Y x} -> Y %search => Z yI created issue #3452 for this |
Description
Added parameters to constraint hints to fix #3448
Should this change go in the CHANGELOG?
implementation, I have updated
CHANGELOG_NEXT.md(and potentially alsoCONTRIBUTORS.md).