Strange type error when using type `result` in satysfi-dist using satysfi-highlight and satysfi-azmath

[yasuo-ozu]

I tried satysfi-highlight, and I encountered a strange error.

@import: satysfi-highlight/highlight/code
@require: azmath/azmath

page-break A1Paper 
    (fun (_) -> ( (| text-height = 1cm; text-origin = (0cm, 0cm); |) ))
    (fun (_) -> (|header-content = block-nil; header-origin = (0cm, 0cm); footer-content = block-nil; footer-origin = (0cm, 0cm); |))
        block-nil

and error:

 ---- ---- ---- ----
  type checking 'result.satyg' ...
! [Warning about pattern-matching] at "result.satyg", line 54, character 4 to line 56, character 15
    pattern #2 is unused

! [Type Error] at "result.satyg", line 61, characters 6-12:
    this expression has type
      'a 'b result,
    but is expected of type
      'a 'b result.
    This constraint is required by the expression
    at "result.satyg", line 59, characters 10-11.

[yasuo-ozu]

satysfi-azmath: 0.0.3 satysfi-highlight: 3d6bad

[elpinal]

In ML, type identifiers such as result can be shadowed so there can legally be 2 or more distinct types of the same name, though there's room to improve the error message.

[gfngfn]

Thanks for reporting. Which version of SATySFi did you use? I tried to reproduce the error, but I couldn’t see the same one by using v0.0.6. A similar error has indeed occurred, however:

  type checking 'option-ext.satyg' ...
! [Type Error] at "option-ext.satyg", line 7, character 0 to line 232, character 3:
    The implementation of value 'ok-or' has type
      '#a -> '#b option -> '#b '#a result
    which is inconsistent with the type required by the signature
      '#a -> '#b option -> '#b '#a result

Note: result seems contained in satysfi-base, not in satysfi-dist.

It is possible that the result is a valid report of an error where two distinct type constructors named result contradict each other, as @elpinal -san mentioned. Indeed, both satysfi-base and satysfi-highlight provide a type constructor named result, so it is probably the case.

[elpinal]

Also, I'm curious about the whole output of satysfi command to know the exact ordering of files being typechecked, which will make the cause clear.

[gfngfn]

If the cause is the contradiction of two type constructors named result, a simple workaround is to make (a forked version of) satysfi-highlight dependent upon satysfi-base and use result contained in satysfi-base instead of providing another result.

More fundamental solution would be to redesign the module system of SATySFi so that name clashes can be avoided with more ease, but it seems taking several months; it is in progress now.

[yasuo-ozu]

Sorry for late reply and thank you for the conversations. I understood that this problem is essentially not a problem of SATySFi. Later discussion about improvement of SATySFi's error message should be done in #262 .