SATySFi icon indicating copy to clipboard operation
SATySFi copied to clipboard

function type wrapped in an type alias cannot be applied

Open nyuichi opened this issue 4 years ago • 1 comments

Given the following code

type 'a id = 'a

module Foo : sig
  val my-id: ('a -> 'a) id
end = struct
  let my-id a = a
end

Foo.my-id ()

the type checker gives the following error

! [Type Error] at "test.saty", line 36, characters 9-18:
    this expression has type
      ('a -> 'a) id (= ('a -> 'a))
    and thus it cannot be applied to arguments.

It seems that the type ('a -> 'a) id which is equivalent to 'a -> 'a is treated as a type of non-arrow kind.

nyuichi avatar Oct 10 '19 16:10 nyuichi

Thank you for reporting. The reported behavior seems due to the following pattern-matching expression, which fails to take type synonyms into consideration: https://github.com/gfngfn/SATySFi/blob/master/src/frontend/typechecker.ml#L702

gfngfn avatar Oct 16 '19 05:10 gfngfn