Andrei Borzenkov authored 1 year ago and Marge Bot committed 1 year ago

This patch is a preparation for @a-binders implementation.  The main changes are:

* Skolemisation is now prepared to deal with @binders.
  See Note [Skolemisation overview] in GHC.Tc.Utils.Unify.
  Most of the action is in
    - Utils.Unify.matchExpectedFunTys
    - Gen.Pat.tcMatchPats
    - Gen.Expr.tcPolyExprCheck
    - Gen.Binds.tcPolyCheck

Some accompanying refactoring:

* I found that funTyConAppTy_maybe was doing a lot of allocation, and
  rejigged userTypeError_maybe to avoid calling it.

Vladislav Zavialov authored 1 year ago and Marge Bot committed 1 year ago

This patch implements the T2T (term-to-type) transformation in patterns.
Patterns that are checked against a visible forall can now be written
without the `type` keyword:

	  \(type t) (x :: t) -> ...   -- old
	  \t (x :: t) -> ...          -- new

The `t` binder is parsed and renamed as a term pattern (Pat), but
then undergoes a conversion to a type pattern (HsTyPat).
See the new function pat_to_type_pat in compiler/GHC/Tc/Gen/Pat.hs

Krzysztof Gogolewski authored 1 year ago and Marge Bot committed 1 year ago

We now require that in 'forall a -> ty', ty has kind TYPE r for some r.
Fixes #24176

Vladislav Zavialov authored 1 year ago and Marge Bot committed 1 year ago

This patch changes type variable lookup rules (lookupTypeOccRn) and
implicit quantification rules (filterInScope) so that variables bound
in the term namespace can be captured at the type level

  {-# LANGUAGE RequiredTypeArguments #-}
  f1 x = g1 @x                -- `x` used in a type application
  f2 x = g2 (undefined :: x)  -- `x` used in a type annotation
  f3 x = g3 (type x)          -- `x` used in an embedded type
  f4 x = ...
    where g4 :: x -> x        -- `x` used in a type signature
          g4 = ...

This change alone does not allow us to accept examples shown above,
but at least it gets them past the renamer.

Vladislav Zavialov authored 1 year ago and Marge Bot committed 1 year ago

This patch implements the T2T (term-to-type) transformation in
expressions. Given a function with a required type argument
	vfun :: forall a -> ...

the user can now call it as
	vfun (Maybe Int)

instead of
	vfun (type (Maybe Int))

The Maybe Int argument is parsed and renamed as a term (HsExpr), but then
undergoes a conversion to a type (HsType).
See the new function expr_to_type in compiler/GHC/Tc/Gen/App.hs
and Note [RequiredTypeArguments and the T2T mapping]

Left as future work: checking for puns.

Vladislav Zavialov authored 2 years ago and Marge Bot committed 1 year ago

This patch implements part 1 of GHC Proposal #281,
introducing explicit `type` patterns and `type` arguments.

Summary of the changes:

1. New extension flag:
     RequiredTypeArguments

2. New user-facing syntax:
     `type p` patterns    (represented by EmbTyPat)
     `type e` expressions (represented by HsEmbTy)

3. Functions with required type arguments (visible forall)
   can now be defined and applied:
      idv :: forall a -> a -> a    -- signature   (relevant change: checkVdqOK in GHC/Tc/Validity.hs)
      idv (type a) (x :: a) = x    -- definition  (relevant change: tcPats in GHC/Tc/Gen/Pat.hs)
      x = idv (type Int) 42        -- usage       (relevant change: tcInstFun in GHC/Tc/Gen/App.hs)

4. template-haskell support:
      TH.TypeE corresponds to HsEmbTy
      TH.TypeP corresponds to EmbTyPat

5. Test cases and a new User's Guide section

Changes *not* included here are the t2t (term-to-type) transformation
and term variable capture; those belong to part 2.