You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
namespace A
export
data X = Xa | Xb
export
data Y : Type where
namespace B
-- if this is uncommmented, errors out like it should
-- foo : X -> Int
-- foo Xa = 0
-- foo Xb = 1
--this doesn't produce an error, but should
foo2 : Y -> Int
foo2 y impossible
Steps to Reproduce
Typecheck
Expected Behavior
- Errors (1)
`-- X.idr line ...:
While processing left hand side of foo2. Y data values are private.
Observed Behavior
OK!
The text was updated successfully, but these errors were encountered:
redfish64
changed the title
when a data type with no values is not public, the typechecker shouldn't be able to prove a value is impossible
when a data type without values is not public, the typechecker shouldn't be able to prove a value is impossible from another module
Nov 7, 2022
redfish64
changed the title
when a data type without values is not public, the typechecker shouldn't be able to prove a value is impossible from another module
when a data type without values is not public, the typechecker shouldn't be able to prove a value is impossible from another namespace
Nov 7, 2022
If you create a non-public datatype with no values in namespace A, then namespace B can see that.
https://gist.github.com/redfish64/9bbc6b34d1136ce4114b7a2b58c62075
Steps to Reproduce
Typecheck
Expected Behavior
Observed Behavior
OK!
The text was updated successfully, but these errors were encountered: