Visible type application
AbandonedPublic

Authored by goldfire on Aug 7 2015, 7:39 AM.

Details

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

Diff Detail

Repository
rGHC Glasgow Haskell Compiler
Branch
wip/type-app
Lint
Lint WarningsExcuse: lint warnings to be fixed
SeverityLocationCodeMessage
Warningcompiler/basicTypes/Id.hs:285TXT3Line Too Long
Warningcompiler/basicTypes/Id.hs:300TXT3Line Too Long
Warningcompiler/deSugar/DsArrows.hs:509TXT3Line Too Long
Warningcompiler/deSugar/DsBinds.hs:189TXT3Line Too Long
Warningcompiler/deSugar/DsMeta.hs:1461TXT3Line Too Long
Warningcompiler/ghci/ByteCodeGen.hs:110TXT3Line Too Long
Warningcompiler/parser/Lexer.x:2178TXT3Line Too Long
Warningcompiler/parser/RdrHsSyn.hs:1095TXT3Line Too Long
Warningcompiler/simplCore/OccurAnal.hs:1758TXT3Line Too Long
Warningcompiler/specialise/SpecConstr.hs:1646TXT3Line Too Long
Warningcompiler/specialise/Specialise.hs:2150TXT3Line Too Long
Warningcompiler/specialise/Specialise.hs:2158TXT3Line Too Long
Warningcompiler/typecheck/TcArrows.hs:365TXT3Line Too Long
Warningcompiler/typecheck/TcBinds.hs:782TXT3Line Too Long
Warningcompiler/typecheck/TcBinds.hs:788TXT3Line Too Long
Warningcompiler/typecheck/TcBinds.hs:1802TXT3Line Too Long
Warningcompiler/typecheck/TcEvidence.hs:1064TXT3Line Too Long
Warningcompiler/typecheck/TcExpr.hs:11TXT3Line Too Long
Warningcompiler/typecheck/TcExpr.hs:167TXT3Line Too Long
Warningcompiler/typecheck/TcExpr.hs:375TXT3Line Too Long
Warningcompiler/typecheck/TcExpr.hs:390TXT3Line Too Long
Warningcompiler/typecheck/TcExpr.hs:971TXT3Line Too Long
Warningcompiler/typecheck/TcExpr.hs:1644TXT3Line Too Long
Warningcompiler/typecheck/TcMatches.hs:106TXT3Line Too Long
Warningcompiler/typecheck/TcMatches.hs:109TXT3Line Too Long
Unit
No Unit Test Coverage
Build Status
Buildable 5203
Build 5444: GHC Patch Validation (amd64/Linux)
Build 5443: arc lint + arc unit
goldfire updated this revision to Diff 3797.Aug 7 2015, 7:39 AM
goldfire retitled this revision from to Visible type application.
goldfire updated this object.
goldfire edited the test plan for this revision. (Show Details)
goldfire added reviewers: simonpj, austin, bgamari.
goldfire updated the Trac tickets for this revision.

Another ugly bit is the ExpOrAct type in TcUnify. I'd love a way to refactor this cleanly and get rid of this unwieldy parameter to matchExpectedFunTys, but I couldn't seem to find the right way to do it without duplicating gobs of code.

The problem is that matchExpectedFunTys needs to deal with quantified types, potentially hiding arrows. As it turns out, it should only ever need to instantiate such types, never skolemise. (All the "expected" types sent into matchExpectedFunTys are deeply skolemised already.) We do not want to deeplyInstantiate, as that might instantiate more type variables than necessary. So we want to instantiate only as much as necessary... but this kind of traversal through the type is already what matchExpectedFunTys does, and I'd prefer not to repeat it. The pain around this is that instantiating makes an oriented HsWrapper, whereas the other operations in matchExpectedFunTys produce coercions. Previously, without instantiating, some clients of matchExpectedFunTys just reversed the coercions. But now that matchExpectedFunTys instantiates, it needs to return an irreversible HsWrapper. So I don't know what to do. What's there now isn't terrible terrible, but I'd like better.

simonpj edited edge metadata.Aug 7 2015, 9:53 AM

I have not reviewed this properly, but here is one thing I tripped over right away: the new HasSigFlag in IdInfo.

Questions. Is this relevant for imported Ids? Is ti relevant after type checking is complete? I suspect the answer is No in both cases. If I'm right it'd be better to put this info the local TcTypeEnv, wouldn't it?

I have not reviewed this properly, but here is one thing I tripped over right away: the new HasSigFlag in IdInfo.

Questions. Is this relevant for imported Ids? Is ti relevant after type checking is complete? I suspect the answer is No in both cases. If I'm right it'd be better to put this info the local TcTypeEnv, wouldn't it?

The flag is needed in essentially one place: when reading an interface file and constructing an Id from the interface file. If we have a HasSigId, then the type variables in the Ids type should be specified (with internal names). Otherwise, they should inferred (with system names). That's it.

But I think that means the answer to both your questions is "Yes". It's relevant for imported Ids during construction. It's relevant after type checking is complete because it needs to go into an interface file. I haven't gone back to the code to look at this closely in response to this question, but my sense is that the refactoring you're suggesting won't work.

OK so the "type was inferred property" persists across modules. That's a viable choice but it is not the only possibility. It would be simpler if every imported Id was ok for explicit type application.

Is the actual design documented anywhere? The paper was silent on cross-module and Haddock etc questions, and it'd be good to have a place where design decisions that are not covered in the paper are documented.

OK so the "type was inferred property" persists across modules. That's a viable choice but it is not the only possibility. It would be simpler if every imported Id was ok for explicit type application.

Is the actual design documented anywhere? The paper was silent on cross-module and Haddock etc questions, and it'd be good to have a place where design decisions that are not covered in the paper are documented.

Yes, it would be quite a bit simpler if every imported id was considered specified. And this doesn't pose any problem with the theory. But it's quite fragile. Take this:

data T a b
type SwapT a b = T b a

class C x where
  meth :: x -> x

instance C (T a b) where
  meth = undefined

swapT :: SwapT  a b
swapT = undefined

foo = meth swapT

Quick: What's the type of foo? Is it T b a? Or is it SwapT a b? To do the instance lookup for meth, we need to unwrap the synonym. But it's possible that GHC is clever enough to assign foo the type SwapT a b. For visible type application, this matters, because the order of the type arguments is taken from the order of type variables in the type. It's quite conceivable that the type inferred for something like foo (or something much more complex!) will change, even between minor revisions of GHC. And yet this could all conceivably break client code that uses visible type application, unbeknownst to the author of the code above. Thus motivated by practicalities, Stephanie and I decided to preserve information about where type signatures exist between modules. This is actually documented in the paper, in the last sentence of section 7.2.

Haddock is a good point: we would need to indicate whether or not a type is user-supplied in the Haddock output. I've added this to my internal notes on things that need to be done.

Well, you clearly need a way to know what the inferred type of foo is. So use Haddock, or -ddump-types, or GHCi and :info foo. (You could imagine a more civilised version of -ddump-types like -dshow-inferred-types.)

But all seem preferable (to me) to this pervasive has-sig flag which needs to be propagated into every tool that consumes Haskell.

Well, you clearly need a way to know what the inferred type of foo is. So use Haddock, or -ddump-types, or GHCi and :info foo. (You could imagine a more civilised version of -ddump-types like -dshow-inferred-types.)

But all seem preferable (to me) to this pervasive has-sig flag which needs to be propagated into every tool that consumes Haskell.

For a given GHC, it's no problem to learn the type of foo. It won't change. Any of the techniques you mention are fine. But I'm worried between GHCs. When you upgrade from 7.12.1 to 7.12.2, it's very conceivable that the type of foo will change. This causes downstream problems. Perhaps users of VTA adopt that burden knowingly. But if we don't track has-sig, then those users don't even know precisely where they're adopting the burden (only on un-sig'd ids). It was thinking along these lines that convinced me we need the indeed-more-annoying has-sig stuff.

All civilised libraries give type sigs for exported functions. So I would only expect this fragility within a package; and you are unlikely to change GHC's without rebuilding the entire package.

Given the pervasiveness of type signatures for exported functions, I'm just doubtful that adding all this extra cross-module stuff is paying its way

Even intra-package module interactions can be problematic here.

But I realized all of this is moot: once this merges with D808, all the specified/inferred stuff moves into the Binder type in that branch, and all the HasSigId stuff goes away. So the behavior as implemented here remains, but the annoyance in the implementation does not.

@goldfire, where can the Cabal changes needed by this patch be found? Perhaps you could update .gitmodules to point to them to enable Harbormaster to validate (I will revert this change before merging).

@goldfire, where can the Cabal changes needed by this patch be found? Perhaps you could update .gitmodules to point to them to enable Harbormaster to validate (I will revert this change before merging).

Thanks for asking. I pushed to ssh://git@git.haskell.org/packages/Cabal.git (the wip/type-app branch), so it should work now.

austin requested changes to this revision.Sep 8 2015, 11:27 AM
austin edited edge metadata.

Hrm.... With the description in the commit, I'm wondering if we should review this as-is. I'd rather have atrociously ugly things never get into the source code at all, we have enough of those. :) Plus it'd be nice to not have to review that just yet: if types-are-kinds is so close, we might as well just review the cleaned version.

Richard, I was meaning to ask this, but what's the timeframe for D808/types-are-kinds? Is it sometime, say, ~1 month or so? Because if so, then perhaps we should simply get that in first. Hopefully that would still leave you with enough time to rebase this, modulo atrocious-stuff. Or have you discussed this recently?

This revision now requires changes to proceed.Sep 8 2015, 11:27 AM

As I've realized the level of the atrocity here, I've become more biased toward folding this into D808, and then abandoning this revision. Thus: don't review!

Timeframe for D808: I'll arbitrarily say 5 weeks.

This is going to folded into D808.

@goldfire, do you suppose you could abandon this diff?

goldfire abandoned this revision.Nov 16 2015, 9:08 PM

Sure.