Track type variable scope more carefully.
authorRichard Eisenberg <rae@cs.brynmawr.edu>
Mon, 4 Sep 2017 21:27:17 +0000 (22:27 +0100)
committerRichard Eisenberg <rae@cs.brynmawr.edu>
Sun, 1 Apr 2018 03:16:46 +0000 (23:16 -0400)
commitfaec8d358985e5d0bf363bd96f23fe76c9e281f7
tree9aebd4566f5787dbbe08ca8fd9dc720958610345
parentca535f95a742d885c4082c9dc296c151fb3c1e12
Track type variable scope more carefully.

The main job of this commit is to track more accurately the scope
of tyvars introduced by user-written foralls. For example, it would
be to have something like this:

  forall a. Int -> (forall k (b :: k). Proxy '[a, b]) -> Bool

In that type, a's kind must be k, but k isn't in scope. We had a
terrible way of doing this before (not worth repeating or describing
here, but see the old tcImplicitTKBndrs and friends), but now
we have a principled approach: make an Implication when kind-checking
a forall. Doing so then hooks into the existing machinery for
preventing skolem-escape, performing floating, etc. This also means
that we bump the TcLevel whenever going into a forall.

The new behavior is done in TcHsType.scopeTyVars, but see also
TcHsType.tc{Im,Ex}plicitTKBndrs, which have undergone significant
rewriting. There are several Notes near there to guide you. Of
particular interest there is that Implication constraints can now
have skolems that are out of order; this situation is reported in
TcErrors.

A major consequence of this is a slightly tweaked process for type-
checking type declarations. The new Note [Use SigTvs in kind-checking
pass] in TcTyClsDecls lays it out.

The error message for dependent/should_fail/TypeSkolEscape has become
noticeably worse. However, this is because the code in TcErrors goes to
some length to preserve pre-8.0 error messages for kind errors. It's time
to rip off that plaster and get rid of much of the kind-error-specific
error messages. I tried this, and doing so led to a lovely error message
for TypeSkolEscape. So: I'm accepting the error message quality regression
for now, but will open up a new ticket to fix it, along with a larger
error-message improvement I've been pondering. This applies also to
dependent/should_fail/{BadTelescope2,T14066,T14066e}, polykinds/T11142.

Other minor changes:
 - isUnliftedTypeKind didn't look for tuples and sums. It does now.

 - check_type used check_arg_type on both sides of an AppTy. But the left
   side of an AppTy isn't an arg, and this was causing a bad error message.
   I've changed it to use check_type on the left-hand side.

 - Some refactoring around when we print (TYPE blah) in error messages.
   The changes decrease the times when we do so, to good effect.
   Of course, this is still all controlled by
   -fprint-explicit-runtime-reps

Fixes #14066 #14749

Test cases: dependent/should_compile/{T14066a,T14749},
            dependent/should_fail/T14066{,c,d,e,f,g,h}
121 files changed:
compiler/basicTypes/DataCon.hs
compiler/basicTypes/Var.hs
compiler/deSugar/DsExpr.hs
compiler/hsSyn/HsDecls.hs
compiler/hsSyn/HsTypes.hs
compiler/iface/IfaceType.hs
compiler/iface/ToIface.hs
compiler/nativeGen/RegAlloc/Liveness.hs
compiler/prelude/PrelNames.hs
compiler/typecheck/TcBinds.hs
compiler/typecheck/TcClassDcl.hs
compiler/typecheck/TcDeriv.hs
compiler/typecheck/TcEnv.hs
compiler/typecheck/TcErrors.hs
compiler/typecheck/TcEvidence.hs
compiler/typecheck/TcHsSyn.hs
compiler/typecheck/TcHsType.hs
compiler/typecheck/TcInstDcls.hs
compiler/typecheck/TcInteract.hs
compiler/typecheck/TcMType.hs
compiler/typecheck/TcPat.hs
compiler/typecheck/TcPatSyn.hs
compiler/typecheck/TcRnDriver.hs
compiler/typecheck/TcRnMonad.hs
compiler/typecheck/TcRnTypes.hs
compiler/typecheck/TcSMonad.hs
compiler/typecheck/TcSigs.hs
compiler/typecheck/TcSimplify.hs
compiler/typecheck/TcSplice.hs
compiler/typecheck/TcTyClsDecls.hs
compiler/typecheck/TcType.hs
compiler/typecheck/TcUnify.hs
compiler/typecheck/TcValidity.hs
compiler/types/Coercion.hs
compiler/types/TyCoRep.hs
compiler/types/TyCoRep.hs-boot
compiler/types/TyCon.hs
compiler/types/Type.hs
compiler/utils/Bag.hs
compiler/utils/Outputable.hs
docs/users_guide/glasgow_exts.rst
testsuite/tests/codeGen/should_fail/T13233.stderr
testsuite/tests/dependent/should_compile/InferDependency.hs [new file with mode: 0644]
testsuite/tests/dependent/should_compile/T11635.hs
testsuite/tests/dependent/should_compile/T14066a.hs [new file with mode: 0644]
testsuite/tests/dependent/should_compile/T14066a.stderr [new file with mode: 0644]
testsuite/tests/dependent/should_compile/T14749.hs [moved from testsuite/tests/typecheck/should_compile/T14749.hs with 100% similarity]
testsuite/tests/dependent/should_compile/all.T
testsuite/tests/dependent/should_fail/BadTelescope.stderr
testsuite/tests/dependent/should_fail/BadTelescope2.stderr
testsuite/tests/dependent/should_fail/BadTelescope3.stderr
testsuite/tests/dependent/should_fail/BadTelescope4.stderr
testsuite/tests/dependent/should_fail/InferDependency.stderr
testsuite/tests/dependent/should_fail/T13601.stderr
testsuite/tests/dependent/should_fail/T13780c.stderr
testsuite/tests/dependent/should_fail/T14066.hs [new file with mode: 0644]
testsuite/tests/dependent/should_fail/T14066.stderr [new file with mode: 0644]
testsuite/tests/dependent/should_fail/T14066c.hs [new file with mode: 0644]
testsuite/tests/dependent/should_fail/T14066c.stderr [new file with mode: 0644]
testsuite/tests/dependent/should_fail/T14066d.hs [new file with mode: 0644]
testsuite/tests/dependent/should_fail/T14066d.stderr [new file with mode: 0644]
testsuite/tests/dependent/should_fail/T14066e.hs [new file with mode: 0644]
testsuite/tests/dependent/should_fail/T14066e.stderr [new file with mode: 0644]
testsuite/tests/dependent/should_fail/T14066f.hs [new file with mode: 0644]
testsuite/tests/dependent/should_fail/T14066f.stderr [new file with mode: 0644]
testsuite/tests/dependent/should_fail/T14066g.hs [new file with mode: 0644]
testsuite/tests/dependent/should_fail/T14066g.stderr [new file with mode: 0644]
testsuite/tests/dependent/should_fail/T14066h.hs [new file with mode: 0644]
testsuite/tests/dependent/should_fail/T14066h.stderr [new file with mode: 0644]
testsuite/tests/dependent/should_fail/TypeSkolEscape.hs
testsuite/tests/dependent/should_fail/TypeSkolEscape.stderr
testsuite/tests/dependent/should_fail/all.T
testsuite/tests/deriving/should_compile/T11732c.hs
testsuite/tests/gadt/T12468.stderr
testsuite/tests/ghci/scripts/T10248.stderr
testsuite/tests/ghci/scripts/T10249.stderr
testsuite/tests/ghci/scripts/T8353.stderr
testsuite/tests/indexed-types/should_fail/T7938.stderr
testsuite/tests/indexed-types/should_fail/T8129.stdout
testsuite/tests/module/mod71.stderr
testsuite/tests/partial-sigs/should_compile/T12531.stderr
testsuite/tests/partial-sigs/should_fail/T10615.stderr
testsuite/tests/partial-sigs/should_fail/T11976.stderr
testsuite/tests/partial-sigs/should_fail/T14040a.stderr
testsuite/tests/perf/haddock/all.T
testsuite/tests/polykinds/SigTvKinds3.hs [new file with mode: 0644]
testsuite/tests/polykinds/SigTvKinds3.stderr [new file with mode: 0644]
testsuite/tests/polykinds/T11142.stderr
testsuite/tests/polykinds/T12593.stderr
testsuite/tests/polykinds/T13985.stderr
testsuite/tests/polykinds/T14563.hs
testsuite/tests/polykinds/T14846.stderr
testsuite/tests/polykinds/T7230.stderr
testsuite/tests/polykinds/T8566.stderr
testsuite/tests/polykinds/T9222.stderr
testsuite/tests/polykinds/all.T
testsuite/tests/th/T10267.stderr
testsuite/tests/typecheck/should_compile/T13050.stderr
testsuite/tests/typecheck/should_compile/T13343.hs
testsuite/tests/typecheck/should_compile/T14590.stderr
testsuite/tests/typecheck/should_compile/T2494.stderr
testsuite/tests/typecheck/should_compile/T9497a.stderr
testsuite/tests/typecheck/should_compile/abstract_refinement_substitutions.stderr
testsuite/tests/typecheck/should_compile/all.T
testsuite/tests/typecheck/should_compile/hole_constraints.stderr
testsuite/tests/typecheck/should_compile/hole_constraints_nested.stderr
testsuite/tests/typecheck/should_compile/holes.stderr
testsuite/tests/typecheck/should_compile/holes3.stderr
testsuite/tests/typecheck/should_compile/refinement_substitutions.stderr
testsuite/tests/typecheck/should_compile/valid_substitutions.stderr
testsuite/tests/typecheck/should_compile/valid_substitutions_interactions.stderr
testsuite/tests/typecheck/should_fail/T11355.stderr
testsuite/tests/typecheck/should_fail/T12177.stderr
testsuite/tests/typecheck/should_fail/T14350.stderr
testsuite/tests/typecheck/should_fail/T14607.hs
testsuite/tests/typecheck/should_fail/T14607.stderr
testsuite/tests/typecheck/should_fail/T9497d.stderr
testsuite/tests/typecheck/should_fail/all.T
testsuite/tests/typecheck/should_run/T9497a-run.stderr
testsuite/tests/typecheck/should_run/T9497b-run.stderr
testsuite/tests/typecheck/should_run/T9497c-run.stderr