Visible type application

Authored by goldfire.

Description

Visible type application

Summary:
This implements visible type application into GHC, as described in
http://www.seas.upenn.edu/~sweirich/papers/type-app-extended.pdf

Very briefly, this means (with new extension TypeApplications
enabled) that you can say show (read @Int "5") and get the
behavior that you want.

This is a sizable change to the type-checker, because it means that
tcExpr does not instantiate types it infers. Instead, types
are instantiated only when required. The details are in the paper.

  • At this point, kind variables may not be visibly instantiated. I

expect to fix this deficiency in the merging type/kind work.

  • Visible type application is not yet available in patterns, only

expressions. I expect to fix this, also.

  • This patch also adds some more tidying to TcValidity, necessary

for good error messages. This actually fixes a bug unrelated to
visible type application.

  • There are some open design questions. I will post to Trac #5296, as

Trac seems a better forum for design issues.

There is one part of this patch which is atrociously ugly. As
described in the paper, we must keep track of the difference between
specified type variables (as given by the user) and inferred type
variables (as generated by GHC). There is not a convenient place to
mark this distinction. BUT, there is a convenient place in my
merging types/kinds patch, which should land for 7.12. So I did
an ugly thing: I put the bit in the Name of the type variable,
using System names for inferred variables and Internal names for
specified ones. This was actually only a small change from existing
practice, but I well know that having type-checking depend on a
variable's Name is terrible. However, I think it's better for this
patch to land separate from my types/kinds patch, and changing
ForAllTy to note the specified/inferred distinction would duplicate
a bunch of effort in my other patch. Thus the compromise seen here.
This behavior will be removed when this patch is merged into my
other one.

If this is just too ugly, I can accept that and merge this with
my other patch internally, without going via master.

Test Plan: ./validate

Reviewers: simonpj, bgamari, austin, hvr

Subscribers: thomie, mpickering

Differential Revision: https://phabricator.haskell.org/D1138

GHC Trac Issues: Trac #5296, Trac #10619, Trac #10589, Trac #10709.

Details

Committed
goldfireAug 7 2015, 7:40 AM
Differential Revision
D1138: Visible type application
Parents
rGHC91db569611f0: Revert "*** Use global url for .gitmodules"
Branches
Unknown
Tags
Unknown