Returning quantified types from type functions is mighty fragile

[plt-amy]

type function foo ('x : bool) begin
  foo true  = forall 'a. 'a -> 'a
  foo false = ()
end

type sbool 'x =
  | STrue  : sbool true
  | SFalse : sbool false

let
  foo :
    forall 'b. sbool 'b -> foo 'b -> ()
  =
    fun x y ->
      match x with
      | STrue -> y @unit ()
      | SFalse -> y

It is reasonable to expect this would type check, but no.

[plt-amy]

Also doesn't work:

-       | STrue -> y @unit ()
+       | STrue -> y ()

Error:

test.ml[16:18 ..16:21]: error (E2001)
   │ 
16 │       | STrue -> y ()
   │                  ^^^^
  Couldn't match actual type forall 'a. 'a -> 'a
    with the type expected by the context, unit -> 'wge

  • Did you apply a function to too many arguments?
  • Note: 
      Where the type,
        forall 'a. 'a -> 'a,
      is the reduction of
        foo 'b

[plt-amy]

Also doesn't work:

-      | STrue -> y @unit ()
+      | STrue -> (y : forall 'a. 'a -> 'a) @unit ()

Error:

test.ml[16:19 ..16:19]: error (E2001)
   │ 
16 │       | STrue -> (y : forall 'a. 'a -> 'a) @unit ()
   │                   ^
  Couldn't match actual type forall 'a. 'a -> 'a
    with the type expected by the context, 'a -> 'a

  • Did you apply a function to too many arguments?
  • Note: 
      Where the type,
        forall 'a. 'a -> 'a,
      is the reduction of
        foo 'b

[plt-amy]

This rephrasing of the program works:

let
  foo :
    forall 'b. sbool 'b -> foo 'b -> ()
  =
    function
      | STrue -> fun (y : forall 'a. 'a -> 'a) -> y ()
      | SFalse -> fun y -> y

[plt-amy]

Possible solution here: https://github.com/AndrasKovacs/elaboration-zoo/tree/master/experimental/poly-instantiation

[plt-amy]

Problem with the possible solution: Core has no dependent types lol

[plt-amy]

What I am going to do is write a warning for this