unison/unison-src/transcripts/fix2350.output.md
2024-07-15 19:10:27 +01:00

1.2 KiB

This tests an issue where ability variables were being defaulted over eagerly. In general, we want to avoid collecting up variables from the use of definitions with types like:

T ->{e} U

Since this type works for every e, it is, 'pure;' and we might as well have e = {}, since {} is a subrow of every other row. However, if e isn't just a quantified variable, but one involved in ongoing inference, it's undesirable to default it. Previously there was a check to see if e occurred in the context. However, the wanted abilities being collected aren't in the context, so types like:

T ->{S e} U ->{e} V

were a corner case. We would add S e to the wanted abilities, then not realize that e shouldn't be defaulted.

unique ability Storage d g where
  save.impl : a ->{Storage d g} ('{g} (d a))

save : a ->{Storage d g, g} (d a)
save a = !(save.impl a)

  Loading changes detected in scratch.u.

  I found and typechecked these definitions in scratch.u. If you
  do an `add` or `update`, here's how your codebase would
  change:
  
    ⍟ These new definitions are ok to `add`:
    
      ability Storage d g
      save : a ->{g, Storage d g} d a