Skip to content
  • Kim Nguyễn's avatar
    Better fix for variable ordering: · e925dc34
    Kim Nguyễn authored
    When computing the result type of a function application ((t→s) • u)  with tallying,
    one first introduces a fresh variable 𝛾 and computes the tallying of
     (t → s) < (u → 𝛾)
    When solving the tallying constraints generated (if that step succeeds),
    variables are taken in some implementation defined order (variables created before
    have a smaller internal id). It is important then that the variables in u
    and 𝛾 are are all before the variables in t and s or all after.
    
    Otherwise, when computing the substitution, variables in u will depend on variables
    in t and s that will in turn depend on gamma (which gives unreadable types).
    e925dc34