Make a smart mkAppTyM

Authored by simonpj on Jan 24 2019, 5:53 AM.

Description

Make a smart mkAppTyM

This patch finally delivers on Trac Trac #15952. Specifically

  • Completely remove Note [The tcType invariant], along with its complicated consequences (IT1-IT6).
  • Replace Note [The well-kinded type invariant] with:

    Note [The Purely Kinded Type Invariant (PKTI)]
  • Instead, establish the (PKTI) in TcHsType.tcInferApps, by using a new function mkAppTyM when building a type application. See Note [mkAppTyM].
  • As a result we can remove the delicate mkNakedXX functions entirely. Specifically, mkNakedCastTy retained lots of extremly delicate Refl coercions which just cluttered everything up, and(worse) were very vulnerable to being silently eliminated by (say) substTy. This led to a succession of bug reports.

The result is noticeably simpler to explain, simpler
to code, and Richard and I are much more confident that
it is correct.

It does not actually fix any bugs, but it brings us closer.
E.g. I hoped it'd fix Trac #15918 and Trac #15799, but it doesn't quite
do so. However, it makes it much easier to fix.

I also did a raft of other minor refactorings:

  • Use tcTypeKind consistently in the type checker
  • Rename tcInstTyBinders to tcInvisibleTyBinders, and refactor it a bit
  • Refactor tcEqType, pickyEqType, tcEqTypeVis Simpler, probably more efficient.
  • Make zonkTcType zonk TcTyCons, at least if they have any free unification variables -- see zonk_tc_tycon in TcMType.zonkTcTypeMapper.

    Not zonking these TcTyCons was actually a bug before.
  • Simplify try_to_reduce_no_cache in TcFlatten (a lot)
  • Combine checkExpectedKind and checkExpectedKindX. And then combine the invisible-binder instantation code Much simpler now.
  • Fix a little bug in TcMType.skolemiseQuantifiedTyVar. I'm not sure how I came across this originally.
  • Fix a little bug in TyCoRep.isUnliftedRuntimeRep (the ASSERT was over-zealous). Again I'm not certain how I encountered this.
  • Add a missing solveLocalEqualities in TcHsType.tcHsPartialSigType. I came across this when trying to get level numbers right.

Details

Committed
simonpjFeb 14 2019, 2:40 AM
Parents
rGHC19626218566e: Implement -Wredundant-record-wildcards and -Wunused-record-wildcards
Branches
Unknown
Tags
Unknown