Open
Description
When writing documentation, the block code syntax sometimes fails to typecheck for ability requirement reasons when none are being used.
myDoc2 = {{
```
ifLeft: Char -> Text
ifLeft c = toText c
ifRight: Nat -> Text
ifRight nat = toText nat
myEither : Either Char Nat
myEither = Left ?z
Either.fold ifLeft ifRight myEither
```
}}
Produces the error:
The expression in red
needs the abilities: {𝕖114}
but was assumed to only require: {𝕖132, 𝕖105}
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.
48 | Either.fold ifLeft ifRight myEither
But it works when entirely inlined
myDoc = {{
```
Either.fold (b -> Char.toText b)(a -> toText (a + 1)) (Left ?a)
```
}}
It works when not in a doc codeblock
ifLeft: Char -> Text
ifLeft c = toText c
ifRight: Nat -> Text
ifRight nat = toText nat
myEither : Either Char Nat
myEither = Left ?z
> Either.fold ifLeft ifRight myEither
And inlining only the offending term will also fix the problem.
myDoc3 = {{
```
ifLeft: Char -> Text
ifLeft c = toText c
myEither : Either Char Nat
myEither = Left ?z
Either.fold ifLeft (nat -> Nat.toText nat) myEither
```
}}
Ucm version: latest-184-g513422a68
Raw text file with these examples:
docAbilityFile.txt