type-scheme-case

[gelisam]

As discussed with @david-christiansen:

We currently have a type-case macro whose scrutinee is a value of type Type. Even though our Hindley–Milner type system does infer polymorphic types for our definitions, it is impossible to observe a forall. Consider the following attempt:

(define my-id
  (lambda (x) x))

-- my-id : ∀(α : *). (α → α) ↦
-- #<closure>
(example my-id)

(define-macro (force-type)
  (>>= (which-problem)
       (lambda (problem)
         (case problem
           [(expression type)
            (type-case type
              [(-> a b)
               (type-case a  -- stuck here
                 [(else _)
                  (pure 'my-id)])])]))))

-- No progress was possible:
--    (AwaitingTypeCase _)
--    (GeneralizeType _ _ _)
(example
  (:: my-id (:: (force-type) (nil))))

my-id has a polymorphic type, but in the list (:: my-id (:: (force-type) (nil)), its type is specialized to ?1 -> ?1. Thus, (force-type)is able to observe that the outer type is a function type, but gets stuck when trying to force the unification variable?1`. This is as-designed: making sure macros get stuck when attempting to force unification variables is the key which ensures that macros cannot behave in fragile ways.

There are cases where pattern-matching on those foralls would be useful. For example, in #157 if we want to support polymorphic implicit conversion functions, we need to pattern-match on the polymorphic type to check if it matches the (-> actual expected) type we are looking for. As another example, we might wish to define a #lang in which polymorphic functions can only be instantiated at types with specific shapes, not at all types, as this makes it possible to implement "non-parametric polymorphism", a runtime type-case which covers all the possible shapes.

The proposed solution is a type-scheme-case macro whose scrutinee is an identifier, not a type. The type-scheme of an identifier is a single forall, a possibly-empty list of universally-quantified type variables, and a type in which those type variables may occur:

`(type-scheme-case 'id
   [(forall (A B C) T)
    (... (type=? A T)
         (type-case T ...))])

Once #155 is implemented, it will be possible to combine type-case and type-equality to examine T and figure out where A, B and C occur inside that type expression.

This should not break predictability, because the type-scheme-case expression obviously needs to block until the Hindley–Milner generalization step has determined which unification variables must be turned into universally-quantified variables. If the scrutinee identifier is bound in a nested let and refers to variables bound in outer lets, T may contain unification variables in addition to occurrences of the bound quantification variables, but type-case and type=? should already handle those well.