hylo-lang / hylo

The Hylo programming language
https://www.hylo-lang.org
Apache License 2.0
1.21k stars 56 forks source link

Inference issue when unexpected type found #1291

Open peter-evans opened 8 months ago

peter-evans commented 8 months ago

In this example from the tour the error is actually error: type 'Int' does not conform to trait 'ExpressibleByFloatLiteral', but should be as described in the code comment.

public fun main() {
  var length = 1
  &length = 2.3 // error: expected type `Int`, found `Float64`
}

Ref: https://github.com/hylo-lang/GitBooks/pull/13/files#r1444448705

kyouko-taiga commented 6 months ago

Below a trace of type inference for the assignment.

I think the problem is that {Int == Float64 ∧ Float64 == Int} produces two distinct error diagnostics whereas {Int : ExpressibleByFloatLiteral ∧ %0.3357 == Int} produces only one. So when the solver processes the disjunction it will conclude that the latter candidate yields a better solution.

I think we should avoid producing a disjunction in the first place. Since we already have an expected type for the RHS operand when we generate constraints for the assignment, I suspect we can produce a better constraint.

test.hylo:38.3-16: type inference for '&length = 2.3'
---
fresh:
- "{%0.3357 == Float64 ∧ Float64 == Int}:0 ∨ {Int : ExpressibleByFloatLiteral ∧ %0.3357 == Int}:1"
- "%0.3357 == Int"
- "Int : Movable"
stale:
steps:
- solve: "Int : Movable"
  actions:
  - success
- solve: "%0.3357 == Int"
  actions:
  - assume: "%0.3357 = Int"
  - success
- solve: "{Int == Float64 ∧ Float64 == Int}:0 ∨ {Int : ExpressibleByFloatLiteral ∧ Int == Int}:1"
  actions:
  - fork:
    - pick: "{Int == Float64 ∧ Float64 == Int}:0"
      - break
      fresh:
      - "Int == Float64"
      - "Float64 == Int"
      stale:
      steps:
      - solve: "Float64 == Int"
        actions:
        - failure
      - solve: "Int == Float64"
        actions:
        - failure
    - pick: "{Int : ExpressibleByFloatLiteral ∧ Int == Int}:1"
      - break
      fresh:
      - "Int : ExpressibleByFloatLiteral"
      - "Int == Int"
      stale:
      steps:
      - solve: "Int == Int"
        actions:
        - success
      - solve: "Int : ExpressibleByFloatLiteral"
        actions:
        - failure
typeAssumptions:
  %0.3357 : Int
bindingAssumptions:
  NameExpr(13520) : direct(VarDecl(13514), [:])
penalties: 1
diagnostics: 1
stale: