Skip to content

Curious ability requirement only in Doc block code  #2302

Open
@rlmark

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

Metadata

Assignees

No one assigned

    Labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions