Skip to content
GitLab

Parser, renamer, type checker for @a-binders (#17594)

Open Andrei Borzenkov requested to merge wip/sand-witch/check-@-binders into master

As a part of GHC Proposal 448 were introduced invisible type patterns (@a-patterns) in functions and lambdas:

  id1 :: a -> a
  id1 @t x = x :: t

  id2 :: a -> a
  id2 = \ @t x -> x :: t

This MR introduces the new data type ArgPat and now Match stores it instead of Pat. ArgPat has two constructors: VisPat for common patterns and InvisPat for @-patterns.

Parsing is implemented in production argpat. Was introduced ArgPatBuilder to help post process new patterns.

Renaming of ArgPat is implemented in rnArgPats function.

Type checking is a bit tricky due to eager scolemisation. It's implemented in new functions tcTopSkolemiseExpPatTys, tcSkolemiseScopedExpPatTys, and tcArgPats. For more information about hack with collecting ExpPatTypes see Note [Type-checking invisible type patterns: check mode]

Type-checking is currently limited by check mode and -XNoDeepSubsumption.

Examples of new code:

  id1 :: forall a. a -> a
  id1 @t x = x :: t

  id2 :: a -> a
  id2 @t x = x :: t

  id3 :: a -> a
  id3 = \ @t x -> x

  id_RankN :: (forall a. a -> a) -> a -> a
  id_RankN @t f = f @t

  id4 = id_RankN \ @t x -> x :: t

  id_list :: [forall a. a -> a]
  id_list = [\ @t x -> x]
Edited by Simon Peyton Jones