Skip to content

Cannot create curried dependent functions #12211

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.

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

Closed
TomasMikula opened this issue Apr 24, 2021 · 0 comments · Fixed by #12214
Closed

Cannot create curried dependent functions #12211

TomasMikula opened this issue Apr 24, 2021 · 0 comments · Fixed by #12214
Milestone

Comments

@TomasMikula
Copy link
Contributor

Compiler version

3.0.0-RC3

Minimized code

def fst[A, B[_]]: (a: A) => (b: B[a.type]) => a.type =
  (a: A) => (b: B[a.type]) => a

def snd[A, B[_]]: (a: A) => (b: B[a.type]) => b.type =
  (a: A) => (b: B[a.type]) => b

Output

-- [E007] Type Mismatch Error: test.scala:2:12 ---------------------------------
2 |  (a: A) => (b: B[a.type]) => a
  |            ^^^^^^^^^^^^^^^^^^^
  |          Found:    B[(a : A)] => A
  |          Required: (b: Nothing) => A & (b: B[(a : A)]) => (a : A)
  |
  |          where:    B is a type in method fst with bounds <: [_$1] =>> Any

longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: test.scala:5:12 ---------------------------------
5 |  (a: A) => (b: B[a.type]) => b
  |            ^^^^^^^^^^^^^^^^^^^
  |          Found:    B[(a : A)] => B[(a : A)]
  |          Required: (b: Nothing) => Any & (b: B[(a : A)]) => b.type
  |
  |          where:    B is a type in method snd with bounds <: [_$2] =>> Any

longer explanation available when compiling with `-explain`
2 errors found

Expectation

The code should compile, as the bodies conform to the type signatures.

Also, I haven't found any way of creating an instance of a dependent function type like (a: A) => (b: B[a.type]) => a.type above.

odersky added a commit to dotty-staging/dotty that referenced this issue Apr 25, 2021
Dependent function types are expressed as refinements over regular function types.
These refinements need to be compared with the standard arrow rule for function
subtyping. But comparison of method refinements so far demanded equal parameter
types.

The solution is tricky since refined types lead to selections via reflection
still cannot tolerate differing parameter types since reflexive method dispatch
uses precise parameter types. That's why we apply standard arrow rule only
for refinements where the refined method exists in the underlying class.

Fixes scala#12211
odersky added a commit to dotty-staging/dotty that referenced this issue Apr 29, 2021
Dependent function types are expressed as refinements over regular function types.
These refinements need to be compared with the standard arrow rule for function
subtyping. But comparison of method refinements so far demanded equal parameter
types.

The solution is tricky since refined types lead to selections via reflection
still cannot tolerate differing parameter types since reflexive method dispatch
uses precise parameter types. That's why we apply standard arrow rule only
for refinements where the refined method exists in the underlying class.

Fixes scala#12211
michelou pushed a commit to michelou/scala3 that referenced this issue May 1, 2021
Dependent function types are expressed as refinements over regular function types.
These refinements need to be compared with the standard arrow rule for function
subtyping. But comparison of method refinements so far demanded equal parameter
types.

The solution is tricky since refined types lead to selections via reflection
still cannot tolerate differing parameter types since reflexive method dispatch
uses precise parameter types. That's why we apply standard arrow rule only
for refinements where the refined method exists in the underlying class.

Fixes scala#12211
michelou pushed a commit to michelou/scala3 that referenced this issue May 2, 2021
Dependent function types are expressed as refinements over regular function types.
These refinements need to be compared with the standard arrow rule for function
subtyping. But comparison of method refinements so far demanded equal parameter
types.

The solution is tricky since refined types lead to selections via reflection
still cannot tolerate differing parameter types since reflexive method dispatch
uses precise parameter types. That's why we apply standard arrow rule only
for refinements where the refined method exists in the underlying class.

Fixes scala#12211
liufengyun pushed a commit to dotty-staging/dotty that referenced this issue May 3, 2021
Dependent function types are expressed as refinements over regular function types.
These refinements need to be compared with the standard arrow rule for function
subtyping. But comparison of method refinements so far demanded equal parameter
types.

The solution is tricky since refined types lead to selections via reflection
still cannot tolerate differing parameter types since reflexive method dispatch
uses precise parameter types. That's why we apply standard arrow rule only
for refinements where the refined method exists in the underlying class.

Fixes scala#12211
@Kordyjan Kordyjan added this to the 3.0.1 milestone Aug 2, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants