unison/unison-src/transcripts-using-base/fix5129.output.md
Dan Doel 34877da01c Don't relax type when doing an instantiateL during subtyping
This is the case of `a < T` for some structured T. By relaxing, we are
actually allowing `a` to be a _supertype_ of T as far as abilities go,
which is not correct. Seems like it was just erroneously mirrored from
the opposite case.
2024-06-25 15:54:10 -04:00

1.6 KiB
Raw Blame History

Checks for some bad type checking behavior. Some ability subtyping was too lenient when higher-order functions were involved.

foreach : (a ->{g} ()) -> [a] ->{g} ()
foreach f = cases
  [] -> ()
  x +: xs ->
    f x
    foreach f xs

forkIt : '{IO} () ->{IO} ()
forkIt e =
  _ = IO.forkComp e
  ()

thunk : '{IO,Exception} ()
thunk = do
  raise (Failure (typeLink MiscFailure) "thunk" (Any ()))

go = do
  foreach forkIt [thunk]

  Loading changes detected in scratch.u.

  I found an ability mismatch when checking the application
  
     18 |   foreach forkIt [thunk]
  
  
  When trying to match [Unit ->{𝕖75, IO, Exception} Unit] with
  [Unit ->{IO} Unit] the left hand side contained extra
  abilities: {𝕖75, Exception}
  
  

This comes from issue #3513

(<<) : (b ->{e} c) -> (a ->{e} b) -> a ->{e} c
(<<) f g x = f (g x)

catchAll.impl : '{IO, Exception} a ->{IO} Either Failure a
catchAll.impl thunk =
  handle tryEval do catch thunk
  with
    cases
      { x }                    -> x
      {Exception.raise f -> _} -> Left f

fancyTryEval : '{g, IO, Exception} a ->{g, IO, Exception} a
fancyTryEval = reraise << catchAll.impl

  Loading changes detected in scratch.u.

  The expression in red
  
                needs the abilities: {g76}
    but was assumed to only require: {IO, Exception}
  
  This is likely a result of using an un-annotated function as an argument with concrete abilities. Try adding an annotation to the function definition whose body is red.
  
     13 | fancyTryEval = reraise << catchAll.impl