Add kind equalities to GHC.
authorRichard Eisenberg <eir@cis.upenn.edu>
Fri, 11 Dec 2015 23:19:53 +0000 (18:19 -0500)
committerRichard Eisenberg <eir@cis.upenn.edu>
Fri, 11 Dec 2015 23:23:12 +0000 (18:23 -0500)
This implements the ideas originally put forward in
"System FC with Explicit Kind Equality" (ICFP'13).

There are several noteworthy changes with this patch:
 * We now have casts in types. These change the kind
   of a type. See new constructor `CastTy`.

 * All types and all constructors can be promoted.
   This includes GADT constructors. GADT pattern matches
   take place in type family equations. In Core,
   types can now be applied to coercions via the
   `CoercionTy` constructor.

 * Coercions can now be heterogeneous, relating types
   of different kinds. A coercion proving `t1 :: k1 ~ t2 :: k2`
   proves both that `t1` and `t2` are the same and also that
   `k1` and `k2` are the same.

 * The `Coercion` type has been significantly enhanced.
   The documentation in `docs/core-spec/core-spec.pdf` reflects
   the new reality.

 * The type of `*` is now `*`. No more `BOX`.

 * Users can write explicit kind variables in their code,
   anywhere they can write type variables. For backward compatibility,
   automatic inference of kind-variable binding is still permitted.

 * The new extension `TypeInType` turns on the new user-facing
   features.

 * Type families and synonyms are now promoted to kinds. This causes
   trouble with parsing `*`, leading to the somewhat awkward new
   `HsAppsTy` constructor for `HsType`. This is dispatched with in
   the renamer, where the kind `*` can be told apart from a
   type-level multiplication operator. Without `-XTypeInType` the
   old behavior persists. With `-XTypeInType`, you need to import
   `Data.Kind` to get `*`, also known as `Type`.

 * The kind-checking algorithms in TcHsType have been significantly
   rewritten to allow for enhanced kinds.

 * The new features are still quite experimental and may be in flux.

 * TODO: Several open tickets: #11195, #11196, #11197, #11198, #11203.

 * TODO: Update user manual.

Tickets addressed: #9017, #9173, #7961, #10524, #8566, #11142.
Updates Haddock submodule.

576 files changed:
.gitmodules
README.md
compiler/basicTypes/BasicTypes.hs
compiler/basicTypes/ConLike.hs
compiler/basicTypes/DataCon.hs
compiler/basicTypes/DataCon.hs-boot
compiler/basicTypes/Id.hs
compiler/basicTypes/IdInfo.hs
compiler/basicTypes/IdInfo.hs-boot
compiler/basicTypes/Lexeme.hs
compiler/basicTypes/MkId.hs
compiler/basicTypes/MkId.hs-boot
compiler/basicTypes/Name.hs
compiler/basicTypes/NameEnv.hs
compiler/basicTypes/OccName.hs
compiler/basicTypes/PatSyn.hs
compiler/basicTypes/PatSyn.hs-boot
compiler/basicTypes/SrcLoc.hs
compiler/basicTypes/Unique.hs
compiler/basicTypes/Var.hs
compiler/basicTypes/VarEnv.hs
compiler/basicTypes/VarSet.hs
compiler/cmm/Cmm.hs
compiler/cmm/CmmExpr.hs
compiler/cmm/CmmLayoutStack.hs
compiler/cmm/Hoopl/Dataflow.hs
compiler/codeGen/StgCmmClosure.hs
compiler/codeGen/StgCmmLayout.hs
compiler/coreSyn/CoreArity.hs
compiler/coreSyn/CoreFVs.hs
compiler/coreSyn/CoreLint.hs
compiler/coreSyn/CorePrep.hs
compiler/coreSyn/CoreSubst.hs
compiler/coreSyn/CoreSyn.hs
compiler/coreSyn/CoreTidy.hs
compiler/coreSyn/CoreUnfold.hs
compiler/coreSyn/CoreUtils.hs
compiler/coreSyn/MkCore.hs
compiler/coreSyn/PprCore.hs
compiler/coreSyn/TrieMap.hs
compiler/deSugar/Check.hs
compiler/deSugar/Desugar.hs
compiler/deSugar/DsArrows.hs
compiler/deSugar/DsBinds.hs
compiler/deSugar/DsCCall.hs
compiler/deSugar/DsExpr.hs
compiler/deSugar/DsForeign.hs
compiler/deSugar/DsGRHSs.hs
compiler/deSugar/DsListComp.hs
compiler/deSugar/DsMeta.hs
compiler/deSugar/DsMonad.hs
compiler/deSugar/DsUtils.hs
compiler/deSugar/Match.hs
compiler/deSugar/MatchCon.hs
compiler/deSugar/PmExpr.hs
compiler/ghc.cabal.in
compiler/ghc.mk
compiler/ghci/ByteCodeGen.hs
compiler/ghci/Debugger.hs
compiler/ghci/DebuggerUtils.hs
compiler/ghci/RtClosureInspect.hs
compiler/hsSyn/Convert.hs
compiler/hsSyn/HsDecls.hs
compiler/hsSyn/HsExpr.hs
compiler/hsSyn/HsPat.hs
compiler/hsSyn/HsTypes.hs
compiler/hsSyn/HsUtils.hs
compiler/iface/BinIface.hs
compiler/iface/BuildTyCl.hs
compiler/iface/IfaceEnv.hs
compiler/iface/IfaceSyn.hs
compiler/iface/IfaceType.hs
compiler/iface/MkIface.hs
compiler/iface/TcIface.hs
compiler/iface/TcIface.hs-boot
compiler/main/Annotations.hs
compiler/main/DynFlags.hs
compiler/main/DynamicLoading.hs
compiler/main/GHC.hs
compiler/main/GhcMonad.hs
compiler/main/GhcPlugins.hs
compiler/main/HscStats.hs
compiler/main/HscTypes.hs
compiler/main/InteractiveEval.hs
compiler/main/InteractiveEvalTypes.hs
compiler/main/PipelineMonad.hs
compiler/main/PprTyThing.hs
compiler/nativeGen/PPC/Ppr.hs
compiler/nativeGen/RegAlloc/Graph/ArchBase.hs
compiler/nativeGen/RegAlloc/Graph/ArchX86.hs
compiler/nativeGen/RegAlloc/Graph/Coalesce.hs
compiler/nativeGen/RegAlloc/Graph/Main.hs
compiler/nativeGen/RegAlloc/Graph/Spill.hs
compiler/nativeGen/RegAlloc/Graph/SpillClean.hs
compiler/nativeGen/RegAlloc/Graph/SpillCost.hs
compiler/nativeGen/RegAlloc/Graph/Stats.hs
compiler/nativeGen/RegAlloc/Linear/Main.hs
compiler/nativeGen/RegAlloc/Linear/PPC/FreeRegs.hs
compiler/nativeGen/RegAlloc/Linear/SPARC/FreeRegs.hs
compiler/nativeGen/RegAlloc/Linear/StackMap.hs
compiler/nativeGen/RegAlloc/Linear/Stats.hs
compiler/nativeGen/SPARC/CodeGen/Gen64.hs
compiler/parser/ApiAnnotation.hs
compiler/parser/Lexer.x
compiler/parser/Parser.y
compiler/parser/RdrHsSyn.hs
compiler/prelude/PrelInfo.hs
compiler/prelude/PrelNames.hs
compiler/prelude/PrelNames.hs-boot
compiler/prelude/PrelRules.hs
compiler/prelude/PrimOp.hs
compiler/prelude/TysPrim.hs
compiler/prelude/TysWiredIn.hs
compiler/prelude/TysWiredIn.hs-boot
compiler/rename/RnEnv.hs
compiler/rename/RnNames.hs
compiler/rename/RnPat.hs
compiler/rename/RnSource.hs
compiler/rename/RnTypes.hs
compiler/simplCore/CSE.hs
compiler/simplCore/CoreMonad.hs
compiler/simplCore/FloatIn.hs
compiler/simplCore/OccurAnal.hs
compiler/simplCore/SAT.hs
compiler/simplCore/SetLevels.hs
compiler/simplCore/SimplEnv.hs
compiler/simplCore/SimplMonad.hs
compiler/simplCore/SimplUtils.hs
compiler/simplCore/Simplify.hs
compiler/simplStg/UnariseStg.hs
compiler/specialise/Rules.hs
compiler/specialise/SpecConstr.hs
compiler/specialise/Specialise.hs
compiler/stgSyn/StgLint.hs
compiler/stranal/DmdAnal.hs
compiler/stranal/WwLib.hs
compiler/typecheck/FamInst.hs
compiler/typecheck/FunDeps.hs
compiler/typecheck/Inst.hs
compiler/typecheck/TcArrows.hs
compiler/typecheck/TcBinds.hs
compiler/typecheck/TcCanonical.hs
compiler/typecheck/TcClassDcl.hs
compiler/typecheck/TcDefaults.hs
compiler/typecheck/TcDeriv.hs
compiler/typecheck/TcEnv.hs
compiler/typecheck/TcErrors.hs
compiler/typecheck/TcEvidence.hs
compiler/typecheck/TcExpr.hs
compiler/typecheck/TcFlatten.hs
compiler/typecheck/TcForeign.hs
compiler/typecheck/TcGenDeriv.hs
compiler/typecheck/TcGenGenerics.hs
compiler/typecheck/TcHsSyn.hs
compiler/typecheck/TcHsType.hs
compiler/typecheck/TcInstDcls.hs
compiler/typecheck/TcInteract.hs
compiler/typecheck/TcMType.hs
compiler/typecheck/TcMatches.hs
compiler/typecheck/TcPat.hs
compiler/typecheck/TcPatSyn.hs
compiler/typecheck/TcPluginM.hs
compiler/typecheck/TcRnDriver.hs
compiler/typecheck/TcRnMonad.hs
compiler/typecheck/TcRnTypes.hs
compiler/typecheck/TcRules.hs
compiler/typecheck/TcSMonad.hs
compiler/typecheck/TcSimplify.hs
compiler/typecheck/TcSplice.hs
compiler/typecheck/TcTyClsDecls.hs
compiler/typecheck/TcTyDecls.hs
compiler/typecheck/TcType.hs
compiler/typecheck/TcType.hs-boot
compiler/typecheck/TcTypeNats.hs
compiler/typecheck/TcTypeable.hs
compiler/typecheck/TcUnify.hs
compiler/typecheck/TcUnify.hs-boot
compiler/typecheck/TcValidity.hs
compiler/types/Class.hs
compiler/types/CoAxiom.hs
compiler/types/Coercion.hs
compiler/types/Coercion.hs-boot [new file with mode: 0644]
compiler/types/FamInstEnv.hs
compiler/types/InstEnv.hs
compiler/types/Kind.hs
compiler/types/OptCoercion.hs
compiler/types/TyCoRep.hs [new file with mode: 0644]
compiler/types/TyCoRep.hs-boot [moved from compiler/types/TypeRep.hs-boot with 68% similarity]
compiler/types/TyCon.hs
compiler/types/Type.hs
compiler/types/Type.hs-boot
compiler/types/TypeRep.hs [deleted file]
compiler/types/Unify.hs
compiler/utils/Bag.hs
compiler/utils/ListSetOps.hs
compiler/utils/MonadUtils.hs
compiler/utils/Outputable.hs
compiler/utils/Pair.hs
compiler/utils/Serialized.hs
compiler/utils/UniqDFM.hs
compiler/utils/UniqDSet.hs
compiler/utils/UniqSet.hs
compiler/utils/Util.hs
compiler/vectorise/Vectorise.hs
compiler/vectorise/Vectorise/Builtins.hs
compiler/vectorise/Vectorise/Builtins/Base.hs
compiler/vectorise/Vectorise/Builtins/Initialise.hs
compiler/vectorise/Vectorise/Convert.hs
compiler/vectorise/Vectorise/Env.hs
compiler/vectorise/Vectorise/Exp.hs
compiler/vectorise/Vectorise/Generic/Description.hs
compiler/vectorise/Vectorise/Generic/PADict.hs
compiler/vectorise/Vectorise/Generic/PAMethods.hs
compiler/vectorise/Vectorise/Generic/PData.hs
compiler/vectorise/Vectorise/Monad.hs
compiler/vectorise/Vectorise/Monad/Base.hs
compiler/vectorise/Vectorise/Monad/Global.hs
compiler/vectorise/Vectorise/Monad/InstEnv.hs
compiler/vectorise/Vectorise/Monad/Local.hs
compiler/vectorise/Vectorise/Monad/Naming.hs
compiler/vectorise/Vectorise/Type/Classify.hs
compiler/vectorise/Vectorise/Type/Env.hs
compiler/vectorise/Vectorise/Type/TyConDecl.hs
compiler/vectorise/Vectorise/Type/Type.hs
compiler/vectorise/Vectorise/Utils.hs
compiler/vectorise/Vectorise/Utils/Base.hs
compiler/vectorise/Vectorise/Utils/Closure.hs
compiler/vectorise/Vectorise/Utils/Hoisting.hs
compiler/vectorise/Vectorise/Utils/PADict.hs
compiler/vectorise/Vectorise/Utils/Poly.hs
compiler/vectorise/Vectorise/Var.hs
compiler/vectorise/Vectorise/Vect.hs
docs/core-spec/.gitignore
docs/core-spec/CoreLint.ott
docs/core-spec/CoreSyn.ott
docs/core-spec/Makefile
docs/core-spec/OpSem.ott
docs/core-spec/core-spec.mng
docs/core-spec/core-spec.pdf
docs/users_guide/glasgow_exts.rst
docs/users_guide/using.rst
libraries/base/Data/Coerce.hs
libraries/base/Data/Kind.hs [new file with mode: 0644]
libraries/base/Data/Monoid.hs
libraries/base/Data/Type/Coercion.hs
libraries/base/Data/Type/Equality.hs
libraries/base/Data/Typeable/Internal.hs
libraries/base/GHC/Base.hs
libraries/base/GHC/Exts.hs
libraries/base/GHC/TypeLits.hs
libraries/base/base.cabal
libraries/base/tests/CatEntail.hs
libraries/ghc-prim/GHC/Classes.hs
libraries/ghc-prim/GHC/Types.hs
rae.txt [new file with mode: 0644]
testsuite/tests/ado/ado004.stderr
testsuite/tests/annotations/should_fail/annfail10.stderr
testsuite/tests/deSugar/should_compile/T2431.stderr
testsuite/tests/deSugar/should_compile/T4488.stderr
testsuite/tests/dependent/Makefile [new file with mode: 0644]
testsuite/tests/dependent/should_compile/Dep1.hs [new file with mode: 0644]
testsuite/tests/dependent/should_compile/Dep2.hs [new file with mode: 0644]
testsuite/tests/dependent/should_compile/Dep3.hs [new file with mode: 0644]
testsuite/tests/dependent/should_compile/KindEqualities.hs [new file with mode: 0644]
testsuite/tests/dependent/should_compile/KindEqualities2.hs [new file with mode: 0644]
testsuite/tests/dependent/should_compile/KindLevels.hs [new file with mode: 0644]
testsuite/tests/dependent/should_compile/Makefile [new file with mode: 0644]
testsuite/tests/dependent/should_compile/RAE_T32b.hs [new file with mode: 0644]
testsuite/tests/dependent/should_compile/Rae31.hs [new file with mode: 0644]
testsuite/tests/dependent/should_compile/RaeBlogPost.hs [new file with mode: 0644]
testsuite/tests/dependent/should_compile/all.T [new file with mode: 0644]
testsuite/tests/dependent/should_compile/mkGADTVars.hs [new file with mode: 0644]
testsuite/tests/dependent/should_fail/BadTelescope.hs [new file with mode: 0644]
testsuite/tests/dependent/should_fail/BadTelescope.stderr [new file with mode: 0644]
testsuite/tests/dependent/should_fail/BadTelescope2.hs [new file with mode: 0644]
testsuite/tests/dependent/should_fail/BadTelescope2.stderr [new file with mode: 0644]
testsuite/tests/dependent/should_fail/BadTelescope3.hs [new file with mode: 0644]
testsuite/tests/dependent/should_fail/BadTelescope3.stderr [new file with mode: 0644]
testsuite/tests/dependent/should_fail/BadTelescope4.hs [new file with mode: 0644]
testsuite/tests/dependent/should_fail/BadTelescope4.stderr [new file with mode: 0644]
testsuite/tests/dependent/should_fail/DepFail1.hs [new file with mode: 0644]
testsuite/tests/dependent/should_fail/DepFail1.stderr [new file with mode: 0644]
testsuite/tests/dependent/should_fail/Makefile [new file with mode: 0644]
testsuite/tests/dependent/should_fail/PromotedClass.hs [new file with mode: 0644]
testsuite/tests/dependent/should_fail/PromotedClass.stderr [new file with mode: 0644]
testsuite/tests/dependent/should_fail/RAE_T32a.hs [new file with mode: 0644]
testsuite/tests/dependent/should_fail/RAE_T32a.stderr [new file with mode: 0644]
testsuite/tests/dependent/should_fail/SelfDep.hs [new file with mode: 0644]
testsuite/tests/dependent/should_fail/SelfDep.stderr [new file with mode: 0644]
testsuite/tests/dependent/should_fail/TypeSkolEscape.hs [new file with mode: 0644]
testsuite/tests/dependent/should_fail/TypeSkolEscape.stderr [new file with mode: 0644]
testsuite/tests/dependent/should_fail/all.T [new file with mode: 0644]
testsuite/tests/deriving/should_compile/T10524.hs [moved from testsuite/tests/deriving/should_fail/T10524.hs with 77% similarity]
testsuite/tests/deriving/should_compile/all.T
testsuite/tests/deriving/should_fail/T1496.stderr
testsuite/tests/deriving/should_fail/T7959.stderr
testsuite/tests/deriving/should_fail/all.T
testsuite/tests/deriving/should_fail/drvfail005.stderr
testsuite/tests/driver/T4437.hs
testsuite/tests/driver/werror.stderr
testsuite/tests/gadt/T3163.stderr
testsuite/tests/gadt/gadt-escape1.stderr
testsuite/tests/gadt/gadt10.stderr
testsuite/tests/gadt/gadt13.stderr
testsuite/tests/gadt/gadt7.stderr
testsuite/tests/ghc-api/annotations/T10307.stdout
testsuite/tests/ghc-api/annotations/T10312.stderr
testsuite/tests/ghc-api/annotations/T10312.stdout
testsuite/tests/ghc-api/annotations/T10357.stderr
testsuite/tests/ghc-api/annotations/T10357.stdout
testsuite/tests/ghc-api/annotations/T10358.stdout
testsuite/tests/ghc-api/annotations/T11018.stderr
testsuite/tests/ghc-api/annotations/T11018.stdout
testsuite/tests/ghc-api/annotations/exampleTest.stdout
testsuite/tests/ghc-api/annotations/listcomps.stdout
testsuite/tests/ghc-api/annotations/parseTree.stdout
testsuite/tests/ghc-api/landmines/landmines.stdout
testsuite/tests/ghci.debugger/scripts/break001.stdout
testsuite/tests/ghci.debugger/scripts/break003.stderr
testsuite/tests/ghci.debugger/scripts/break003.stdout
testsuite/tests/ghci.debugger/scripts/break006.stderr
testsuite/tests/ghci.debugger/scripts/break006.stdout
testsuite/tests/ghci.debugger/scripts/break012.stdout
testsuite/tests/ghci.debugger/scripts/break018.stdout
testsuite/tests/ghci.debugger/scripts/break022/break022.stdout
testsuite/tests/ghci.debugger/scripts/break026.stdout
testsuite/tests/ghci.debugger/scripts/break028.stdout
testsuite/tests/ghci.debugger/scripts/hist001.stdout
testsuite/tests/ghci.debugger/scripts/print018.stdout
testsuite/tests/ghci.debugger/scripts/print022.stdout
testsuite/tests/ghci.debugger/scripts/print025.stdout
testsuite/tests/ghci.debugger/scripts/print031.stdout
testsuite/tests/ghci.debugger/scripts/print036.stdout
testsuite/tests/ghci/prog009/ghci.prog009.stdout
testsuite/tests/ghci/scripts/Defer02.stderr
testsuite/tests/ghci/scripts/Defer02.stdout
testsuite/tests/ghci/scripts/T10122.stdout
testsuite/tests/ghci/scripts/T10508.stderr
testsuite/tests/ghci/scripts/T2182ghci.stderr
testsuite/tests/ghci/scripts/T4087.stdout
testsuite/tests/ghci/scripts/T4175.stdout
testsuite/tests/ghci/scripts/T6018ghcifail.stderr
testsuite/tests/ghci/scripts/T7627.stdout
testsuite/tests/ghci/scripts/T7730.stdout
testsuite/tests/ghci/scripts/T7873.script
testsuite/tests/ghci/scripts/T7873.stderr [new file with mode: 0644]
testsuite/tests/ghci/scripts/T7873.stdout
testsuite/tests/ghci/scripts/T7939.stdout
testsuite/tests/ghci/scripts/T9181.stdout
testsuite/tests/ghci/scripts/ghci001.stdout
testsuite/tests/ghci/scripts/ghci013.stdout
testsuite/tests/ghci/scripts/ghci047.stderr
testsuite/tests/ghci/scripts/ghci051.stderr
testsuite/tests/ghci/scripts/ghci055.stdout
testsuite/tests/ghci/scripts/ghci059.script
testsuite/tests/ghci/scripts/ghci059.stdout
testsuite/tests/haddock/should_compile_flag_haddock/haddockA023.stderr
testsuite/tests/haddock/should_compile_flag_haddock/haddockA026.stderr
testsuite/tests/haddock/should_compile_flag_haddock/haddockA027.stderr
testsuite/tests/haddock/should_compile_flag_haddock/haddockA028.stderr
testsuite/tests/indexed-types/should_compile/PushedInAsGivens.stderr
testsuite/tests/indexed-types/should_compile/Simple12.hs
testsuite/tests/indexed-types/should_compile/T3017.stderr
testsuite/tests/indexed-types/should_compile/T3208b.stderr
testsuite/tests/indexed-types/should_compile/T9316.hs
testsuite/tests/indexed-types/should_compile/T9747.hs
testsuite/tests/indexed-types/should_fail/ClosedFam3.stderr
testsuite/tests/indexed-types/should_fail/Overlap4.stderr
testsuite/tests/indexed-types/should_fail/SimpleFail12.stderr
testsuite/tests/indexed-types/should_fail/SimpleFail14.stderr
testsuite/tests/indexed-types/should_fail/SimpleFail1a.stderr
testsuite/tests/indexed-types/should_fail/SimpleFail1b.stderr
testsuite/tests/indexed-types/should_fail/SimpleFail6.stderr
testsuite/tests/indexed-types/should_fail/T10141.stderr
testsuite/tests/indexed-types/should_fail/T10899.stderr
testsuite/tests/indexed-types/should_fail/T2627b.stderr
testsuite/tests/indexed-types/should_fail/T2664.stderr
testsuite/tests/indexed-types/should_fail/T3330a.stderr
testsuite/tests/indexed-types/should_fail/T3330c.stderr
testsuite/tests/indexed-types/should_fail/T4179.stderr
testsuite/tests/indexed-types/should_fail/T5439.stderr
testsuite/tests/indexed-types/should_fail/T6123.stderr
testsuite/tests/indexed-types/should_fail/T7786.stderr
testsuite/tests/indexed-types/should_fail/T7788.stderr
testsuite/tests/indexed-types/should_fail/T9160.stderr
testsuite/tests/indexed-types/should_fail/T9171.stderr
testsuite/tests/indexed-types/should_fail/T9357.stderr
testsuite/tests/indexed-types/should_run/T5719.hs
testsuite/tests/mdo/should_compile/mdo006.hs
testsuite/tests/module/mod71.stderr
testsuite/tests/module/mod72.stderr
testsuite/tests/parser/should_compile/read014.stderr
testsuite/tests/parser/should_fail/T3811d.stderr
testsuite/tests/parser/should_fail/T7848.stderr
testsuite/tests/parser/should_fail/readFail003.stderr
testsuite/tests/partial-sigs/should_compile/ADT.stderr
testsuite/tests/partial-sigs/should_compile/DataFamilyInstanceLHS.stderr
testsuite/tests/partial-sigs/should_compile/Meltdown.stderr
testsuite/tests/partial-sigs/should_compile/SkipMany.stderr
testsuite/tests/partial-sigs/should_compile/T10403.stderr
testsuite/tests/partial-sigs/should_compile/T10438.stderr
testsuite/tests/partial-sigs/should_compile/T11192.stderr
testsuite/tests/partial-sigs/should_compile/TypeFamilyInstanceLHS.stderr
testsuite/tests/partial-sigs/should_compile/WarningWildcardInstantiations.stderr
testsuite/tests/partial-sigs/should_fail/T10045.stderr
testsuite/tests/partial-sigs/should_fail/WildcardInstantiations.stderr
testsuite/tests/patsyn/should_fail/T9161-2.stderr
testsuite/tests/perf/compiler/all.T
testsuite/tests/perf/haddock/all.T
testsuite/tests/polykinds/PolyInstances.hs [new file with mode: 0644]
testsuite/tests/polykinds/PolyKinds02.stderr
testsuite/tests/polykinds/PolyKinds04.stderr
testsuite/tests/polykinds/PolyKinds07.stderr
testsuite/tests/polykinds/SigTvKinds.hs [new file with mode: 0644]
testsuite/tests/polykinds/SigTvKinds2.hs [new file with mode: 0644]
testsuite/tests/polykinds/SigTvKinds2.stderr [new file with mode: 0644]
testsuite/tests/polykinds/T10503.stderr
testsuite/tests/polykinds/T11142.hs [new file with mode: 0644]
testsuite/tests/polykinds/T11142.stderr [new file with mode: 0644]
testsuite/tests/polykinds/T5716.hs
testsuite/tests/polykinds/T5716.stderr
testsuite/tests/polykinds/T6021.hs
testsuite/tests/polykinds/T6021.stderr
testsuite/tests/polykinds/T6039.stderr [deleted file]
testsuite/tests/polykinds/T6129.stderr
testsuite/tests/polykinds/T7224.stderr
testsuite/tests/polykinds/T7230.stderr
testsuite/tests/polykinds/T7278.hs
testsuite/tests/polykinds/T7278.stderr
testsuite/tests/polykinds/T7328.hs
testsuite/tests/polykinds/T7328.stderr
testsuite/tests/polykinds/T7341.hs
testsuite/tests/polykinds/T7341.stderr
testsuite/tests/polykinds/T7404.stderr
testsuite/tests/polykinds/T7438.stderr
testsuite/tests/polykinds/T7481.stderr [deleted file]
testsuite/tests/polykinds/T7524.stderr
testsuite/tests/polykinds/T7594.hs
testsuite/tests/polykinds/T7805.stderr
testsuite/tests/polykinds/T7939a.stderr
testsuite/tests/polykinds/T8566.stderr
testsuite/tests/polykinds/T8616.stderr
testsuite/tests/polykinds/T9200b.stderr
testsuite/tests/polykinds/T9222.stderr
testsuite/tests/polykinds/T9569.hs
testsuite/tests/polykinds/all.T
testsuite/tests/rename/should_fail/T2993.stderr
testsuite/tests/rename/should_fail/rnfail026.stderr
testsuite/tests/rename/should_fail/rnfail055.stderr
testsuite/tests/roles/should_compile/Roles1.stderr
testsuite/tests/roles/should_compile/Roles13.stderr
testsuite/tests/roles/should_compile/Roles14.stderr
testsuite/tests/roles/should_compile/Roles2.stderr
testsuite/tests/roles/should_compile/Roles3.stderr
testsuite/tests/roles/should_compile/Roles4.stderr
testsuite/tests/roles/should_compile/T8958.stderr
testsuite/tests/roles/should_compile/all.T
testsuite/tests/rts/T9045.hs
testsuite/tests/simplCore/should_compile/Makefile
testsuite/tests/simplCore/should_compile/T7360.stderr
testsuite/tests/simplCore/should_compile/T8274.stdout
testsuite/tests/simplCore/should_compile/T9400.stderr
testsuite/tests/simplCore/should_compile/rule2.stderr
testsuite/tests/simplCore/should_compile/spec-inline.stderr
testsuite/tests/stranal/sigs/DmdAnalGADTs.stderr
testsuite/tests/stranal/sigs/T8569.stderr
testsuite/tests/th/T3177a.stderr
testsuite/tests/th/T3920.hs
testsuite/tests/th/T7021a.hs
testsuite/tests/th/T8953.stderr
testsuite/tests/th/TH_RichKinds.hs
testsuite/tests/th/TH_RichKinds.stderr
testsuite/tests/th/TH_Roles2.stderr
testsuite/tests/typecheck/should_compile/T5581.hs
testsuite/tests/typecheck/should_compile/T5655.hs
testsuite/tests/typecheck/should_compile/T9834.stderr
testsuite/tests/typecheck/should_compile/T9939.stderr
testsuite/tests/typecheck/should_compile/tc141.stderr
testsuite/tests/typecheck/should_compile/tc167.stderr
testsuite/tests/typecheck/should_compile/tc211.stderr
testsuite/tests/typecheck/should_compile/tc231.stderr
testsuite/tests/typecheck/should_compile/tc243.stderr
testsuite/tests/typecheck/should_compile/tc255.hs
testsuite/tests/typecheck/should_compile/tc256.hs
testsuite/tests/typecheck/should_compile/tc257.hs
testsuite/tests/typecheck/should_compile/tc258.hs
testsuite/tests/typecheck/should_fail/AssocTyDef04.stderr
testsuite/tests/typecheck/should_fail/AssocTyDef06.hs
testsuite/tests/typecheck/should_fail/AssocTyDef06.stderr
testsuite/tests/typecheck/should_fail/FrozenErrorTests.stderr
testsuite/tests/typecheck/should_fail/T10285.stderr
testsuite/tests/typecheck/should_fail/T11112.stderr
testsuite/tests/typecheck/should_fail/T1633.hs
testsuite/tests/typecheck/should_fail/T1633.stderr
testsuite/tests/typecheck/should_fail/T2994.stderr
testsuite/tests/typecheck/should_fail/T3540.stderr
testsuite/tests/typecheck/should_fail/T3950.stderr
testsuite/tests/typecheck/should_fail/T4875.stderr
testsuite/tests/typecheck/should_fail/T5570.stderr
testsuite/tests/typecheck/should_fail/T5853.stderr
testsuite/tests/typecheck/should_fail/T6018fail.stderr
testsuite/tests/typecheck/should_fail/T6018failclosed.stderr
testsuite/tests/typecheck/should_fail/T7368.stderr
testsuite/tests/typecheck/should_fail/T7368a.stderr
testsuite/tests/typecheck/should_fail/T7410.stderr
testsuite/tests/typecheck/should_fail/T7453.stderr
testsuite/tests/typecheck/should_fail/T7609.stderr
testsuite/tests/typecheck/should_fail/T7645.stderr
testsuite/tests/typecheck/should_fail/T7696.stderr
testsuite/tests/typecheck/should_fail/T7734.stderr
testsuite/tests/typecheck/should_fail/T7778.stderr
testsuite/tests/typecheck/should_fail/T7857.stderr
testsuite/tests/typecheck/should_fail/T7892.stderr
testsuite/tests/typecheck/should_fail/T8030.stderr
testsuite/tests/typecheck/should_fail/T8262.stderr
testsuite/tests/typecheck/should_fail/T8514.stderr
testsuite/tests/typecheck/should_fail/T8603.stderr
testsuite/tests/typecheck/should_fail/T8806.stderr
testsuite/tests/typecheck/should_fail/T9109.stderr
testsuite/tests/typecheck/should_fail/T9196.stderr
testsuite/tests/typecheck/should_fail/T9201.stderr
testsuite/tests/typecheck/should_fail/T9260.stderr
testsuite/tests/typecheck/should_fail/T9999.stderr
testsuite/tests/typecheck/should_fail/TcCoercibleFail.stderr
testsuite/tests/typecheck/should_fail/TcCoercibleFail2.hs
testsuite/tests/typecheck/should_fail/TcCoercibleFail2.stderr
testsuite/tests/typecheck/should_fail/tcfail002.stderr
testsuite/tests/typecheck/should_fail/tcfail004.stderr
testsuite/tests/typecheck/should_fail/tcfail005.stderr
testsuite/tests/typecheck/should_fail/tcfail010.stderr
testsuite/tests/typecheck/should_fail/tcfail013.stderr
testsuite/tests/typecheck/should_fail/tcfail014.stderr
testsuite/tests/typecheck/should_fail/tcfail018.stderr
testsuite/tests/typecheck/should_fail/tcfail032.stderr
testsuite/tests/typecheck/should_fail/tcfail036.hs
testsuite/tests/typecheck/should_fail/tcfail036.stderr
testsuite/tests/typecheck/should_fail/tcfail049.stderr
testsuite/tests/typecheck/should_fail/tcfail050.stderr
testsuite/tests/typecheck/should_fail/tcfail057.stderr
testsuite/tests/typecheck/should_fail/tcfail070.stderr
testsuite/tests/typecheck/should_fail/tcfail078.stderr
testsuite/tests/typecheck/should_fail/tcfail088.stderr
testsuite/tests/typecheck/should_fail/tcfail090.stderr
testsuite/tests/typecheck/should_fail/tcfail099.stderr
testsuite/tests/typecheck/should_fail/tcfail113.stderr
testsuite/tests/typecheck/should_fail/tcfail122.stderr
testsuite/tests/typecheck/should_fail/tcfail123.stderr
testsuite/tests/typecheck/should_fail/tcfail132.stderr
testsuite/tests/typecheck/should_fail/tcfail133.stderr
testsuite/tests/typecheck/should_fail/tcfail140.stderr
testsuite/tests/typecheck/should_fail/tcfail146.stderr
testsuite/tests/typecheck/should_fail/tcfail147.stderr
testsuite/tests/typecheck/should_fail/tcfail151.stderr
testsuite/tests/typecheck/should_fail/tcfail159.stderr
testsuite/tests/typecheck/should_fail/tcfail160.stderr
testsuite/tests/typecheck/should_fail/tcfail161.stderr
testsuite/tests/typecheck/should_fail/tcfail181.stderr
testsuite/tests/typecheck/should_fail/tcfail184.stderr
testsuite/tests/typecheck/should_fail/tcfail195.stderr
testsuite/tests/typecheck/should_fail/tcfail196.stderr
testsuite/tests/typecheck/should_fail/tcfail197.stderr
testsuite/tests/typecheck/should_fail/tcfail200.stderr
testsuite/tests/typecheck/should_fail/tcfail201.stderr
testsuite/tests/typecheck/should_fail/tcfail212.stderr
testsuite/tests/typecheck/should_fail/tcfail213.hs
testsuite/tests/typecheck/should_fail/tcfail214.hs
testsuite/tests/typecheck/should_fail/tcfail217.stderr
testsuite/tests/typecheck/should_run/T10284.hs
testsuite/tests/typecheck/should_run/T10284.stderr
testsuite/tests/typecheck/should_run/T10284.stdout
testsuite/tests/typecheck/should_run/T7861.stdout
testsuite/tests/typecheck/should_run/tcrun043.hs
testsuite/tests/typecheck/should_run/tcrun044.hs
testsuite/tests/warnings/should_compile/T11077.stderr
utils/genprimopcode/Main.hs
utils/haddock

index 73ce0d1..26b4fa0 100644 (file)
 [submodule "libraries/binary"]
        path = libraries/binary
-       url = ../packages/binary.git
+       url = http://git.haskell.org/packages/binary.git
        ignore = untracked
 [submodule "libraries/bytestring"]
        path = libraries/bytestring
-       url = ../packages/bytestring.git
+       url = http://git.haskell.org/packages/bytestring.git
        ignore = untracked
 [submodule "libraries/Cabal"]
        path = libraries/Cabal
-       url = ../packages/Cabal.git
+       url = http://git.haskell.org/packages/Cabal.git
        ignore = untracked
 [submodule "libraries/containers"]
        path = libraries/containers
-       url = ../packages/containers.git
+       url = http://git.haskell.org/packages/containers.git
        ignore = untracked
 [submodule "libraries/haskeline"]
        path = libraries/haskeline
-       url = ../packages/haskeline.git
+       url = http://git.haskell.org/packages/haskeline.git
        ignore = untracked
 [submodule "libraries/pretty"]
        path = libraries/pretty
-       url = ../packages/pretty.git
+       url = http://git.haskell.org/packages/pretty.git
        ignore = untracked
 [submodule "libraries/terminfo"]
        path = libraries/terminfo
-       url = ../packages/terminfo.git
+       url = http://git.haskell.org/packages/terminfo.git
        ignore = untracked
 [submodule "libraries/transformers"]
        path = libraries/transformers
-       url = ../packages/transformers.git
+       url = http://git.haskell.org/packages/transformers.git
        ignore = untracked
 [submodule "libraries/xhtml"]
        path = libraries/xhtml
-       url = ../packages/xhtml.git
+       url = http://git.haskell.org/packages/xhtml.git
        ignore = untracked
 [submodule "libraries/Win32"]
        path = libraries/Win32
-       url = ../packages/Win32.git
+       url = http://git.haskell.org/packages/Win32.git
        ignore = untracked
 [submodule "libraries/primitive"]
        path = libraries/primitive
-       url = ../packages/primitive.git
+       url = http://git.haskell.org/packages/primitive.git
        ignore = untracked
 [submodule "libraries/vector"]
        path = libraries/vector
-       url = ../packages/vector.git
+       url = http://git.haskell.org/packages/vector.git
        ignore = untracked
 [submodule "libraries/time"]
        path = libraries/time
-       url = ../packages/time.git
+       url = http://git.haskell.org/packages/time.git
        ignore = untracked
 [submodule "libraries/random"]
        path = libraries/random
-       url = ../packages/random.git
+       url = http://git.haskell.org/packages/random.git
        ignore = untracked
 [submodule "libraries/array"]
        path = libraries/array
-       url = ../packages/array.git
+       url = http://git.haskell.org/packages/array.git
        ignore = none
 [submodule "libraries/deepseq"]
        path = libraries/deepseq
-       url = ../packages/deepseq.git
+       url = http://git.haskell.org/packages/deepseq.git
        ignore = none
 [submodule "libraries/directory"]
        path = libraries/directory
-       url = ../packages/directory.git
+       url = http://git.haskell.org/packages/directory.git
        ignore = none
 [submodule "libraries/filepath"]
        path = libraries/filepath
-       url = ../packages/filepath.git
+       url = http://git.haskell.org/packages/filepath.git
        ignore = none
 [submodule "libraries/hoopl"]
        path = libraries/hoopl
-       url = ../packages/hoopl.git
+       url = http://git.haskell.org/packages/hoopl.git
        ignore = none
 [submodule "libraries/hpc"]
        path = libraries/hpc
-       url = ../packages/hpc.git
+       url = http://git.haskell.org/packages/hpc.git
        ignore = none
 [submodule "libraries/process"]
        path = libraries/process
-       url = ../packages/process.git
+       url = http://git.haskell.org/packages/process.git
        ignore = none
 [submodule "libraries/unix"]
        path = libraries/unix
-       url = ../packages/unix.git
+       url = http://git.haskell.org/packages/unix.git
        ignore = none
 [submodule "libraries/parallel"]
        path = libraries/parallel
-       url = ../packages/parallel.git
+       url = http://git.haskell.org/packages/parallel.git
        ignore = none
 [submodule "libraries/stm"]
        path = libraries/stm
-       url = ../packages/stm.git
+       url = http://git.haskell.org/packages/stm.git
        ignore = none
 [submodule "libraries/dph"]
        path = libraries/dph
-       url = ../packages/dph.git
+       url = http://git.haskell.org/packages/dph.git
        ignore = none
 [submodule "utils/haddock"]
        path = utils/haddock
-       url = ../haddock.git
+       url = http://git.haskell.org/haddock.git
        ignore = none
        branch = ghc-head
 [submodule "nofib"]
        path = nofib
-       url = ../nofib.git
+       url = http://git.haskell.org/nofib.git
        ignore = none
 [submodule "utils/hsc2hs"]
        path = utils/hsc2hs
-       url = ../hsc2hs.git
+       url = http://git.haskell.org/hsc2hs.git
        ignore = none
 [submodule "libffi-tarballs"]
        path = libffi-tarballs
-       url = ../libffi-tarballs.git
+       url = http://git.haskell.org/libffi-tarballs.git
        ignore = none
 [submodule ".arc-linters/arcanist-external-json-linter"]
        path = .arc-linters/arcanist-external-json-linter
index 227657f..ac97f34 100644 (file)
--- a/README.md
+++ b/README.md
@@ -1,39 +1,91 @@
-The Glasgow Haskell Compiler
-============================
+Dependent Types Branch of GHC
+=============================
 
-[![Build Status](https://api.travis-ci.org/ghc/ghc.svg?branch=master)](http://travis-ci.org/ghc/ghc)
+This is a fork of GHC, with work toward supporting dependent types.
+Anyone is welcome to download and play with this implementation,
+and I am happy to receive feedback and issue reports on GitHub.
 
-This is the source tree for [GHC][1], a compiler and interactive
-environment for the Haskell functional programming language.
+There are two options of using this branch:  manual, and Nix-based.
 
-For more information, visit [GHC's web site][1].
+Manual
+------
+
+This code should build, but I have tested it only on `DEBUG` settings;
+I recommend using build style `devel2` in `build.mk`.
+
+Here is a minimal script you can follow to build this at home;
+see the [GHC Building Guide] [3] for more info.
+
+~~~
+git clone https://github.com/goldfirere/ghc.git
+cd ghc
+git checkout nokinds
+git remote set-url origin git://git.haskell.org/ghc.git   # so submodules work
+git submodule update --init
+cd mk
+cp build.mk.sample build.mk
+## edit build.mk to uncomment the line to choose the `devel2` configuration
+cd ..
+perl boot
+./configure
+make
+~~~
+
+Check out the `testsuite/tests/dependent/should_compile` directory for
+a few sample programs that should compile on this fork of GHC.
+
+For more information about GHC, visit [GHC's web site][1].
 
 Information for developers of GHC can be found on the [GHC Trac][2].
 
+Nix-based
+---------
+
+Thanks to @deepfire, this branch is available in Nixpkgs, which means that with
+some effort it can be fairly automatically employed to build any package from
+Hackage.  This way, though, requires that one installs the Nix package manager in
+parallel with the system package manager -- and this option is currently
+unavailable on Windows.
+
+Here are the instructions:
+
+1. To install the Nix package manager, taking over /nix for package storage:
+
+        curl https://nixos.org/nix/install | sh
+
+2. Make Nix use the `master` repository of Nixpkgs package definitions:
 
-Getting the Source
-==================
+       git clone https://github.com/NixOS/nixpkgs.git
+       pushd ~/.nix-defexpr
+       rm -rf channels
+       ln -s ../nixpkgs
+       popd
+       echo 'export NIX_PATH=nixpkgs=/home/---<USERNAME>---/nixpkgs' >> ~/.bashrc
+       export NIX_PATH=nixpkgs=/home/---<USERNAME>---/nixpkgs
 
-There are two ways to get a source tree:
+3. [OPTIONAL] To enable prebuilt binaries from Peter Simons/NixOS Hydra servers:
 
- 1. *Download source tarballs*
+       sudo mkdir /etc/nix
+       echo 'binary-caches = http://hydra.nixos.org/ http://hydra.cryp.to/' | sudo dd of=/etc/nix/nix.conf
 
-  Download the GHC source distribution:
+       # If you don't do that, everything will still work, just it'll have
+       # to build everything from source.
 
-        ghc-<version>-src.tar.bz2
+4. Enter a shell with `ghc-nokinds` available:
 
-  which contains GHC itself and the "boot" libraries.
+        nix-shell -p haskell.compiler.ghcNokinds
 
- 2. *Check out the source code from git*
+5. See it's indeed `nokinds`:
 
-        $ git clone --recursive git://git.haskell.org/ghc.git
+       wget https://raw.githubusercontent.com/goldfirere/ghc/nokinds/testsuite/tests/dependent/should_compile/KindEqualities2.hs
+       runhaskell KindEqualities2.hs
 
-  Note: cloning GHC from Github requires a special setup. See [Getting a GHC
-  repository from Github] [7].
+To apply 'nokinds' to building packages from Hackage, the best option would be
+to follow instructions from the "Nix loves Haskell" talk by Peter Simons:
 
-  **DO NOT submit pull request directly to the github repo.**
-  *See the GHC team's working conventions re [how to contribute a patch to GHC](http://ghc.haskell.org/trac/ghc/wiki/WorkingConventions/FixingBugs "ghc.haskell.org/trac/ghc/wiki/WorkingConventions/FixingBug").*
+   http://cryp.to/nixos-meetup-3-slides.pdf
 
+..where the relevant compiler name would be "ghcNokinds".
 
 Building & Installing
 =====================
index ae51d07..4133eac 100644 (file)
@@ -413,6 +413,10 @@ isBoxed :: Boxity -> Bool
 isBoxed Boxed   = True
 isBoxed Unboxed = False
 
+instance Outputable Boxity where
+  ppr Boxed   = text "Boxed"
+  ppr Unboxed = text "Unboxed"
+
 {-
 ************************************************************************
 *                                                                      *
index 7ff075c..09ad68b 100644 (file)
@@ -32,7 +32,7 @@ import Unique
 import Util
 import Name
 import BasicTypes
-import TypeRep (Type, ThetaType)
+import TyCoRep (Type, ThetaType)
 import Var
 import Type (mkTyConApp)
 
@@ -169,7 +169,7 @@ conLikeResTy (PatSynCon ps)    tys = patSynInstResTy ps tys
 --
 -- 7) The original result type
 conLikeFullSig :: ConLike
-               -> ([TyVar], [TyVar], [(TyVar,Type)]
+               -> ([TyVar], [TyVar], [EqSpec]
                   , ThetaType, ThetaType, [Type], Type)
 conLikeFullSig (RealDataCon con) =
   let (univ_tvs, ex_tvs, eq_spec, theta, arg_tys, res_ty) = dataConFullSig con
index 6e69a1c..712a9b2 100644 (file)
@@ -15,19 +15,23 @@ module DataCon (
         StrictnessMark(..),
         ConTag,
 
+        -- ** Equality specs
+        EqSpec, mkEqSpec, eqSpecTyVar, eqSpecType,
+        eqSpecPair, eqSpecPreds,
+        substEqSpec,
+
         -- ** Field labels
         FieldLbl(..), FieldLabel, FieldLabelString,
 
         -- ** Type construction
-        mkDataCon, fIRST_TAG,
-        buildAlgTyCon,
+        mkDataCon, buildAlgTyCon, fIRST_TAG,
 
         -- ** Type deconstruction
         dataConRepType, dataConSig, dataConInstSig, dataConFullSig,
         dataConName, dataConIdentity, dataConTag, dataConTyCon,
         dataConOrigTyCon, dataConUserType,
         dataConUnivTyVars, dataConExTyVars, dataConAllTyVars,
-        dataConEqSpec, eqSpecPreds, dataConTheta,
+        dataConEqSpec, dataConTheta,
         dataConStupidTheta,
         dataConInstArgTys, dataConOrigArgTys, dataConOrigResTy,
         dataConInstOrigArgTys, dataConRepArgTys,
@@ -45,37 +49,32 @@ module DataCon (
         isNullarySrcDataCon, isNullaryRepDataCon, isTupleDataCon, isUnboxedTupleCon,
         isVanillaDataCon, classDataCon, dataConCannotMatch,
         isBanged, isMarkedStrict, eqHsBang, isSrcStrict, isSrcUnpacked,
+        specialPromotedDc, isLegacyPromotableDataCon, isLegacyPromotableTyCon,
 
         -- ** Promotion related functions
-        promoteDataCon, promoteDataCon_maybe,
-        promoteType, promoteKind,
-        isPromotableType, computeTyConPromotability,
+        promoteDataCon
     ) where
 
 #include "HsVersions.h"
 
 import {-# SOURCE #-} MkId( DataConBoxer )
 import Type
-import ForeignCall( CType )
-import TypeRep( Type(..) )  -- Used in promoteType
-import PrelNames( liftedTypeKindTyConKey )
+import ForeignCall ( CType )
 import Coercion
-import Kind
 import Unify
 import TyCon
 import FieldLabel
 import Class
 import Name
+import PrelNames
+import NameEnv
 import Var
 import Outputable
-import Unique
 import ListSetOps
 import Util
 import BasicTypes
 import FastString
 import Module
-import VarEnv
-import NameSet
 import Binary
 
 import qualified Data.Data as Data
@@ -299,11 +298,11 @@ data DataCon
                 --       syntax, provided its type looks like the above.
                 --       The declaration format is held in the TyCon (algTcGadtSyntax)
 
-        dcUnivTyVars :: [TyVar],        -- Universally-quantified type vars [a,b,c]
+        dcUnivTyVars   :: [TyVar],      -- Universally-quantified type vars [a,b,c]
                                         -- INVARIANT: length matches arity of the dcRepTyCon
                                         ---           result type of (rep) data con is exactly (T a b c)
 
-        dcExTyVars   :: [TyVar],        -- Existentially-quantified type vars
+        dcExTyVars     :: [TyVar],    -- Existentially-quantified type vars
                 -- In general, the dcUnivTyVars are NOT NECESSARILY THE SAME AS THE TYVARS
                 -- FOR THE PARENT TyCon. With GADTs the data con might not even have
                 -- the same number of type variables.
@@ -313,8 +312,9 @@ data DataCon
         -- INVARIANT: the UnivTyVars and ExTyVars all have distinct OccNames
         -- Reason: less confusing, and easier to generate IfaceSyn
 
-        dcEqSpec :: [(TyVar,Type)],     -- Equalities derived from the result type,
-                                        -- _as written by the programmer_
+        dcEqSpec :: [EqSpec],   -- Equalities derived from the result type,
+                                -- _as written by the programmer_
+
                 -- This field allows us to move conveniently between the two ways
                 -- of representing a GADT constructor's type:
                 --      MkT :: forall a b. (a ~ [b]) => b -> T a
@@ -377,8 +377,10 @@ data DataCon
         dcRep      :: DataConRep,
 
         -- Cached
-        dcRepArity    :: Arity,  -- == length dataConRepArgTys
-        dcSourceArity :: Arity,  -- == length dcOrigArgTys
+          -- dcRepArity == length dataConRepArgTys
+        dcRepArity    :: Arity,
+          -- dcSourceArity == length dcOrigArgTys
+        dcSourceArity :: Arity,
 
         -- Result type of constructor is T t1..tn
         dcRepTyCon  :: TyCon,           -- Result tycon, T
@@ -402,8 +404,8 @@ data DataCon
                                 -- Used for Template Haskell and 'deriving' only
                                 -- The actual fixity is stored elsewhere
 
-        dcPromoted :: Promoted TyCon    -- The promoted TyCon if this DataCon is promotable
-                                        -- See Note [Promoted data constructors] in TyCon
+        dcPromoted :: TyCon    -- The promoted TyCon
+                               -- See Note [Promoted data constructors] in TyCon
   }
   deriving Data.Typeable.Typeable
 
@@ -496,6 +498,40 @@ data SrcUnpackedness = SrcUnpack -- ^ {-# UNPACK #-} specified
 -- of the DataCon *worker* fields
 data StrictnessMark = MarkedStrict | NotMarkedStrict
 
+-- | An 'EqSpec' is a tyvar/type pair representing an equality made in
+-- rejigging a GADT constructor
+data EqSpec = EqSpec TyVar
+                     Type
+
+-- | Make an 'EqSpec'
+mkEqSpec :: TyVar -> Type -> EqSpec
+mkEqSpec tv ty = EqSpec tv ty
+
+eqSpecTyVar :: EqSpec -> TyVar
+eqSpecTyVar (EqSpec tv _) = tv
+
+eqSpecType :: EqSpec -> Type
+eqSpecType (EqSpec _ ty) = ty
+
+eqSpecPair :: EqSpec -> (TyVar, Type)
+eqSpecPair (EqSpec tv ty) = (tv, ty)
+
+eqSpecPreds :: [EqSpec] -> ThetaType
+eqSpecPreds spec = [ mkPrimEqPred (mkTyVarTy tv) ty
+                   | EqSpec tv ty <- spec ]
+
+-- | Substitute in an 'EqSpec'. Precondition: if the LHS of the EqSpec
+-- is mapped in the substitution, it is mapped to a type variable, not
+-- a full type.
+substEqSpec :: TCvSubst -> EqSpec -> EqSpec
+substEqSpec subst (EqSpec tv ty)
+  = EqSpec tv' (substTy subst ty)
+  where
+    tv' = getTyVar "substEqSpec" (substTyVar subst tv)
+
+instance Outputable EqSpec where
+  ppr (EqSpec tv ty) = ppr (tv, ty)
+
 {- Note [Bangs on data constructor arguments]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider
@@ -674,14 +710,13 @@ isMarkedStrict _               = True   -- All others are strict
 -- | Build a new data constructor
 mkDataCon :: Name
           -> Bool           -- ^ Is the constructor declared infix?
-          -> Promoted TyConRepName -- ^ Whether promoted, and if so the TyConRepName
-                                   --   for the promoted TyCon
+          -> TyConRepName   -- ^  TyConRepName for the promoted TyCon
           -> [HsSrcBang]    -- ^ Strictness/unpack annotations, from user
           -> [FieldLabel]   -- ^ Field labels for the constructor,
                             -- if it is a record, otherwise empty
           -> [TyVar]        -- ^ Universally quantified type variables
           -> [TyVar]        -- ^ Existentially quantified type variables
-          -> [(TyVar,Type)] -- ^ GADT equalities
+          -> [EqSpec]       -- ^ GADT equalities
           -> ThetaType      -- ^ Theta-type occuring before the arguments proper
           -> [Type]         -- ^ Original argument types
           -> Type           -- ^ Original result type
@@ -725,7 +760,7 @@ mkDataCon name declared_infix prom_info
                   dcRep = rep,
                   dcSourceArity = length orig_arg_tys,
                   dcRepArity = length rep_arg_tys,
-                  dcPromoted = mb_promoted }
+                  dcPromoted = promoted }
 
         -- The 'arg_stricts' passed to mkDataCon are simply those for the
         -- source-language arguments.  We add extra ones for the
@@ -733,20 +768,15 @@ mkDataCon name declared_infix prom_info
 
     tag = assoc "mkDataCon" (tyConDataCons rep_tycon `zip` [fIRST_TAG..]) con
     rep_arg_tys = dataConRepArgTys con
-    rep_ty = mkForAllTys univ_tvs $ mkForAllTys ex_tvs $
+    rep_ty = mkInvForAllTys univ_tvs $ mkInvForAllTys ex_tvs $
              mkFunTys rep_arg_tys $
              mkTyConApp rep_tycon (mkTyVarTys univ_tvs)
 
-    mb_promoted   -- See Note [Promoted data constructors] in TyCon
-      = case prom_info of
-          NotPromoted     -> NotPromoted
-          Promoted rep_nm -> Promoted (mkPromotedDataCon con name rep_nm prom_kind prom_roles)
-    prom_kind  = promoteType (dataConUserType con)
-    prom_roles = map (const Nominal)          (univ_tvs ++ ex_tvs) ++
-                 map (const Representational) orig_arg_tys
+    promoted   -- See Note [Promoted data constructors] in TyCon
+      = mkPromotedDataCon con name prom_info (dataConUserType con) roles
 
-eqSpecPreds :: [(TyVar,Type)] -> ThetaType
-eqSpecPreds spec = [ mkEqPred (mkTyVarTy tv) ty | (tv,ty) <- spec ]
+    roles = map (const Nominal) (univ_tvs ++ ex_tvs) ++
+            map (const Representational) orig_arg_tys
 
 -- | The 'Name' of the 'DataCon', giving it a unique, rooted identification
 dataConName :: DataCon -> Name
@@ -791,11 +821,30 @@ dataConAllTyVars (MkData { dcUnivTyVars = univ_tvs, dcExTyVars = ex_tvs })
   = univ_tvs ++ ex_tvs
 
 -- | Equalities derived from the result type of the data constructor, as written
--- by the programmer in any GADT declaration
-dataConEqSpec :: DataCon -> [(TyVar,Type)]
-dataConEqSpec = dcEqSpec
-
--- | The *full* constraints on the constructor type
+-- by the programmer in any GADT declaration. This includes *all* GADT-like
+-- equalities, including those written in by hand by the programmer.
+dataConEqSpec :: DataCon -> [EqSpec]
+dataConEqSpec (MkData { dcEqSpec = eq_spec, dcOtherTheta = theta })
+  = eq_spec ++
+    [ spec   -- heterogeneous equality
+    | Just (tc, [_k1, _k2, ty1, ty2]) <- map splitTyConApp_maybe theta
+    , tc `hasKey` heqTyConKey
+    , spec <- case (getTyVar_maybe ty1, getTyVar_maybe ty2) of
+                    (Just tv1, _) -> [mkEqSpec tv1 ty2]
+                    (_, Just tv2) -> [mkEqSpec tv2 ty1]
+                    _             -> []
+    ] ++
+    [ spec   -- homogeneous equality
+    | Just (tc, [_k, ty1, ty2]) <- map splitTyConApp_maybe theta
+    , tc `hasKey` eqTyConKey
+    , spec <- case (getTyVar_maybe ty1, getTyVar_maybe ty2) of
+                    (Just tv1, _) -> [mkEqSpec tv1 ty2]
+                    (_, Just tv2) -> [mkEqSpec tv2 ty1]
+                    _             -> []
+    ]
+
+
+-- | The *full* constraints on the constructor type.
 dataConTheta :: DataCon -> ThetaType
 dataConTheta (MkData { dcEqSpec = eq_spec, dcOtherTheta = theta })
   = eqSpecPreds eq_spec ++ theta
@@ -906,10 +955,9 @@ dataConBoxer _ = Nothing
 --
 -- 4) The /original/ result type of the 'DataCon'
 dataConSig :: DataCon -> ([TyVar], ThetaType, [Type], Type)
-dataConSig (MkData {dcUnivTyVars = univ_tvs, dcExTyVars = ex_tvs,
-                    dcEqSpec = eq_spec, dcOtherTheta  = theta,
-                    dcOrigArgTys = arg_tys, dcOrigResTy = res_ty})
-  = (univ_tvs ++ ex_tvs, eqSpecPreds eq_spec ++ theta, arg_tys, res_ty)
+dataConSig con@(MkData {dcUnivTyVars = univ_tvs, dcExTyVars = ex_tvs,
+                        dcOrigArgTys = arg_tys, dcOrigResTy = res_ty})
+  = (univ_tvs ++ ex_tvs, dataConTheta con, arg_tys, res_ty)
 
 dataConInstSig
   :: DataCon
@@ -926,7 +974,7 @@ dataConInstSig (MkData { dcUnivTyVars = univ_tvs, dcExTyVars = ex_tvs
     , substTheta subst (eqSpecPreds eq_spec ++ theta)
     , substTys   subst arg_tys)
   where
-    univ_subst = zipTopTvSubst univ_tvs univ_tys
+    univ_subst = zipOpenTCvSubst univ_tvs univ_tys
     (subst, ex_tvs') = mapAccumL Type.substTyVarBndr univ_subst ex_tvs
 
 
@@ -936,7 +984,7 @@ dataConInstSig (MkData { dcUnivTyVars = univ_tvs, dcExTyVars = ex_tvs
 --
 -- 2) The result of 'dataConExTyVars'
 --
--- 3) The result of 'dataConEqSpec'
+-- 3) The GADT equalities
 --
 -- 4) The result of 'dataConDictTheta'
 --
@@ -945,7 +993,7 @@ dataConInstSig (MkData { dcUnivTyVars = univ_tvs, dcExTyVars = ex_tvs
 --
 -- 6) The original result type of the 'DataCon'
 dataConFullSig :: DataCon
-               -> ([TyVar], [TyVar], [(TyVar,Type)], ThetaType, [Type], Type)
+               -> ([TyVar], [TyVar], [EqSpec], ThetaType, [Type], Type)
 dataConFullSig (MkData {dcUnivTyVars = univ_tvs, dcExTyVars = ex_tvs,
                         dcEqSpec = eq_spec, dcOtherTheta = theta,
                         dcOrigArgTys = arg_tys, dcOrigResTy = res_ty})
@@ -972,11 +1020,12 @@ dataConUserType :: DataCon -> Type
 --
 -- NB: If the constructor is part of a data instance, the result type
 -- mentions the family tycon, not the internal one.
-dataConUserType  (MkData { dcUnivTyVars = univ_tvs,
-                           dcExTyVars = ex_tvs, dcEqSpec = eq_spec,
-                           dcOtherTheta = theta, dcOrigArgTys = arg_tys,
-                           dcOrigResTy = res_ty })
-  = mkForAllTys ((univ_tvs `minusList` map fst eq_spec) ++ ex_tvs) $
+dataConUserType (MkData { dcUnivTyVars = univ_tvs,
+                          dcExTyVars = ex_tvs, dcEqSpec = eq_spec,
+                          dcOtherTheta = theta, dcOrigArgTys = arg_tys,
+                          dcOrigResTy = res_ty })
+  = mkInvForAllTys ((univ_tvs `minusList` map eqSpecTyVar eq_spec) ++
+                    ex_tvs) $
     mkFunTys theta $
     mkFunTys arg_tys $
     res_ty
@@ -1020,8 +1069,9 @@ dataConInstOrigArgTys dc@(MkData {dcOrigArgTys = arg_tys,
 dataConOrigArgTys :: DataCon -> [Type]
 dataConOrigArgTys dc = dcOrigArgTys dc
 
--- | Returns the arg types of the worker, including *all* evidence, after any
--- flattening has been done and without substituting for any type variables
+-- | Returns the arg types of the worker, including *all*
+-- evidence, after any flattening has been done and without substituting for
+-- any type variables
 dataConRepArgTys :: DataCon -> [Type]
 dataConRepArgTys (MkData { dcRep = rep
                          , dcEqSpec = eq_spec
@@ -1051,6 +1101,34 @@ isUnboxedTupleCon (MkData {dcRepTyCon = tc}) = isUnboxedTupleTyCon tc
 isVanillaDataCon :: DataCon -> Bool
 isVanillaDataCon dc = dcVanilla dc
 
+-- | Should this DataCon be allowed in a type even without -XDataKinds?
+-- Currently, only Lifted & Unlifted
+specialPromotedDc :: DataCon -> Bool
+specialPromotedDc dc
+  = dc `hasKey` liftedDataConKey ||
+    dc `hasKey` unliftedDataConKey
+
+-- | Was this datacon promotable before GHC 8.0? That is, is it promotable
+-- without -XTypeInType
+isLegacyPromotableDataCon :: DataCon -> Bool
+isLegacyPromotableDataCon dc
+  =  null (dataConEqSpec dc)  -- no GADTs
+  && null (dataConTheta dc)   -- no context
+  && not (isFamInstTyCon (dataConTyCon dc))   -- no data instance constructors
+  && all isLegacyPromotableTyCon (nameEnvElts $
+                                  tyConsOfType (dataConUserType dc))
+
+-- | Was this tycon promotable before GHC 8.0? That is, is it promotable
+-- without -XTypeInType
+isLegacyPromotableTyCon :: TyCon -> Bool
+isLegacyPromotableTyCon tc
+  = isVanillaAlgTyCon tc ||
+      -- This returns True more often than it should, but it's quite painful
+      -- to make this fully accurate. And no harm is caused; we just don't
+      -- require -XTypeInType every time we need to. (We'll always require
+      -- -XDataKinds, though, so there's no standards-compliance issue.)
+    isFunTyCon tc || isKindTyCon tc
+
 classDataCon :: Class -> DataCon
 classDataCon clas = case tyConDataCons (classTyCon clas) of
                       (dict_constr:no_more) -> ASSERT( null no_more ) dict_constr
@@ -1060,8 +1138,6 @@ dataConCannotMatch :: [Type] -> DataCon -> Bool
 -- Returns True iff the data con *definitely cannot* match a
 --                  scrutinee of type (T tys)
 --                  where T is the dcRepTyCon for the data con
--- NB: look at *all* equality constraints, not only those
---     in dataConEqSpec; see Trac #5168
 dataConCannotMatch tys con
   | null inst_theta   = False   -- Common
   | all isTyVarTy tys = False   -- Also common
@@ -1071,161 +1147,22 @@ dataConCannotMatch tys con
 
     -- TODO: could gather equalities from superclasses too
     predEqs pred = case classifyPredType pred of
-                     EqPred NomEq ty1 ty2 -> [(ty1, ty2)]
-                     _                    -> []
+                     EqPred NomEq ty1 ty2       -> [(ty1, ty2)]
+                     ClassPred eq [_, ty1, ty2]
+                       | eq `hasKey` eqTyConKey -> [(ty1, ty2)]
+                     _                          -> []
 
 {-
-************************************************************************
-*                                                                      *
-                 Promotion
-
-   These functions are here because
-   - isPromotableTyCon calls dataConFullSig
-   - mkDataCon calls promoteType
-   - It's nice to keep the promotion stuff together
+%************************************************************************
+%*                                                                      *
+        Promoting of data types to the kind level
 *                                                                      *
 ************************************************************************
 
-Note [The overall promotion story]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Here is the overall plan.
-
-* Compared to a TyCon T, the promoted 'T has
-     same Name (and hence Unique)
-     same TyConRepName
-  In future the two will collapse into one anyhow.
-
-* Compared to a DataCon K, the promoted 'K (a type constructor) has
-      same Name (and hence Unique)
-  But it has a fresh TyConRepName; after all, the DataCon doesn't have
-  a TyConRepName at all.  (See Note [Grand plan for Typeable] in TcTypeable
-  for TyConRepName.)
-
-  Why does 'K have the same unique as K?  It's acceptable because we don't
-  mix types and terms, so we won't get them confused.  And it's helpful mainly
-  so that we know when to print 'K as a qualified name in error message. The
-  PrintUnqualified stuff depends on whether K is lexically in scope.. but 'K
-  never is!
-
-* It follows that the tick-mark (eg 'K) is not part of the Occ name of
-  either promoted data constructors or type constructors. Instead,
-  pretty-printing: the pretty-printer prints a tick in front of
-     - promoted DataCons (always)
-     - promoted TyCons (with -dppr-debug)
-  See TyCon.pprPromotionQuote
-
-* For a promoted data constructor K, the pipeline goes like this:
-    User writes (in a type):      K or 'K
-    Parser produces OccName:      K{tc} or K{d}, respectively
-    Renamer makes Name:           M.K{d}_r62   (i.e. same unique as DataCon K)
-                                     and K{tc} has been turned into K{d}
-                                     provided it was unambiguous
-    Typechecker makes TyCon:      PromotedDataCon MK{d}_r62
-
-
-Note [Checking whether a group is promotable]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We only want to promote a TyCon if all its data constructors
-are promotable; it'd be very odd to promote some but not others.
-
-But the data constructors may mention this or other TyCons.
-
-So we treat the recursive uses as all OK (ie promotable) and
-do one pass to check that each TyCon is promotable.
-
-Currently type synonyms are not promotable, though that
-could change.
 -}
 
 promoteDataCon :: DataCon -> TyCon
-promoteDataCon (MkData { dcPromoted = Promoted tc }) = tc
-promoteDataCon dc = pprPanic "promoteDataCon" (ppr dc)
-
-promoteDataCon_maybe :: DataCon -> Promoted TyCon
-promoteDataCon_maybe (MkData { dcPromoted = mb_tc }) = mb_tc
-
-computeTyConPromotability :: NameSet -> TyCon -> Bool
-computeTyConPromotability rec_tycons tc
-  =  isAlgTyCon tc    -- Only algebraic; not even synonyms
-                     -- (we could reconsider the latter)
-  && ok_kind (tyConKind tc)
-  && case algTyConRhs tc of
-       DataTyCon { data_cons = cs } -> all ok_con cs
-       TupleTyCon { data_con = c }  -> ok_con c
-       NewTyCon { data_con = c }    -> ok_con c
-       AbstractTyCon {}             -> False
-  where
-    ok_kind kind = all isLiftedTypeKind args && isLiftedTypeKind res
-            where  -- Checks for * -> ... -> * -> *
-              (args, res) = splitKindFunTys kind
-
-    -- See Note [Promoted data constructors] in TyCon
-    ok_con con = all (isLiftedTypeKind . tyVarKind) ex_tvs
-              && null eq_spec   -- No constraints
-              && null theta
-              && all (isPromotableType rec_tycons) orig_arg_tys
-       where
-         (_, ex_tvs, eq_spec, theta, orig_arg_tys, _) = dataConFullSig con
-
-
-isPromotableType :: NameSet -> Type -> Bool
--- Must line up with promoteType
--- But the function lives here because we must treat the
--- *recursive* tycons as promotable
-isPromotableType rec_tcs con_arg_ty
-  = go con_arg_ty
-  where
-    go (TyConApp tc tys) =  tys `lengthIs` tyConArity tc
-                         && (tyConName tc `elemNameSet` rec_tcs
-                             || isPromotableTyCon tc)
-                         && all go tys
-    go (FunTy arg res)   = go arg && go res
-    go (TyVarTy {})      = True
-    go _                 = False
-
-{-
-Note [Promoting a Type to a Kind]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Suppsoe we have a data constructor D
-     D :: forall (a:*). Maybe a -> T a
-We promote this to be a type constructor 'D:
-     'D :: forall (k:BOX). 'Maybe k -> 'T k
-
-The transformation from type to kind is done by promoteType
-
-  * Convert forall (a:*) to forall (k:BOX), and substitute
-
-  * Ensure all foralls are at the top (no higher rank stuff)
-
-  * Ensure that all type constructors mentioned (Maybe and T
-    in the example) are promotable; that is, they have kind
-          * -> ... -> * -> *
--}
-
--- | Promotes a type to a kind.
--- Assumes the argument satisfies 'isPromotableType'
-promoteType :: Type -> Kind
-promoteType ty
-  = mkForAllTys kvs (go rho)
-  where
-    (tvs, rho) = splitForAllTys ty
-    kvs = [ mkKindVar (tyVarName tv) superKind | tv <- tvs ]
-    env = zipVarEnv tvs kvs
-
-    go (TyConApp tc tys) | Promoted prom_tc <- promotableTyCon_maybe tc
-                         = mkTyConApp prom_tc (map go tys)
-    go (FunTy arg res)   = mkArrowKind (go arg) (go res)
-    go (TyVarTy tv)      | Just kv <- lookupVarEnv env tv
-                         = TyVarTy kv
-    go _ = panic "promoteType"  -- Argument did not satisfy isPromotableType
-
-promoteKind :: Kind -> SuperKind
--- Promote the kind of a type constructor
--- from (* -> * -> *) to (BOX -> BOX -> BOX)
-promoteKind (TyConApp tc [])
-  | tc `hasKey` liftedTypeKindTyConKey = superKind
-promoteKind (FunTy arg res) = FunTy (promoteKind arg) (promoteKind res)
-promoteKind k = pprPanic "promoteKind" (ppr k)
+promoteDataCon (MkData { dcPromoted = tc }) = tc
 
 {-
 ************************************************************************
@@ -1283,22 +1220,13 @@ buildAlgTyCon :: Name
               -> ThetaType             -- ^ Stupid theta
               -> AlgTyConRhs
               -> RecFlag
-              -> Bool                  -- ^ True <=> this TyCon is promotable
               -> Bool                  -- ^ True <=> was declared in GADT syntax
               -> AlgTyConFlav
               -> TyCon
 
 buildAlgTyCon tc_name ktvs roles cType stupid_theta rhs
-              is_rec is_promotable gadt_syn parent
-  = tc
+              is_rec gadt_syn parent
+  = mkAlgTyCon tc_name kind ktvs roles cType stupid_theta
+               rhs parent is_rec gadt_syn
   where
-    kind = mkPiKinds ktvs liftedTypeKind
-
-    -- tc and mb_promoted_tc are mutually recursive
-    tc = mkAlgTyCon tc_name kind ktvs roles cType stupid_theta
-                    rhs parent is_rec gadt_syn
-                    mb_promoted_tc
-
-    mb_promoted_tc
-      | is_promotable = Promoted (mkPromotedTyCon tc (promoteKind kind))
-      | otherwise     = NotPromoted
+    kind = mkPiTypesPreferFunTy ktvs liftedTypeKind
index 615ef53..d609774 100644 (file)
@@ -6,10 +6,13 @@ import FieldLabel ( FieldLabel )
 import Unique ( Uniquable )
 import Outputable ( Outputable, OutputableBndr )
 import BasicTypes (Arity)
-import {-# SOURCE #-} TypeRep (Type, ThetaType)
+import {-# SOURCE #-} TyCoRep (Type, ThetaType)
 
 data DataCon
 data DataConRep
+data EqSpec
+eqSpecTyVar :: EqSpec -> TyVar
+
 dataConName      :: DataCon -> Name
 dataConTyCon     :: DataCon -> TyCon
 dataConExTyVars  :: DataCon -> [TyVar]
@@ -18,7 +21,7 @@ dataConFieldLabels :: DataCon -> [FieldLabel]
 dataConInstOrigArgTys  :: DataCon -> [Type] -> [Type]
 dataConStupidTheta :: DataCon -> ThetaType
 dataConFullSig :: DataCon
-               -> ([TyVar], [TyVar], [(TyVar,Type)], ThetaType, [Type], Type)
+               -> ([TyVar], [TyVar], [EqSpec], ThetaType, [Type], Type)
 
 instance Eq DataCon
 instance Ord DataCon
index b49a816..775a77b 100644 (file)
@@ -17,7 +17,7 @@
 --
 -- * 'Name.Name': see "Name#name_types"
 --
--- * 'Id.Id' represents names that not only have a 'Name.Name' but also a 'TypeRep.Type' and some additional
+-- * 'Id.Id' represents names that not only have a 'Name.Name' but also a 'TyCoRep.Type' and some additional
 --   details (a 'IdInfo.IdInfo' and one of 'Var.LocalIdDetails' or 'IdInfo.GlobalIdDetails') that
 --   are added, modified and inspected by various compiler passes. These 'Var.Var' names may either
 --   be global or local, see "Var#globalvslocal"
@@ -30,11 +30,14 @@ module Id (
 
         -- ** Simple construction
         mkGlobalId, mkVanillaGlobal, mkVanillaGlobalWithInfo,
-        mkLocalId, mkLocalIdWithInfo, mkExportedLocalId,
-        mkSysLocal, mkSysLocalM, mkUserLocal, mkUserLocalM,
-        mkDerivedLocalM,
+        mkLocalId, mkLocalCoVar, mkLocalIdOrCoVar,
+        mkLocalIdOrCoVarWithInfo,
+        mkLocalIdWithInfo, mkExportedLocalId,
+        mkSysLocal, mkSysLocalM, mkSysLocalOrCoVar, mkSysLocalOrCoVarM,
+        mkUserLocal, mkUserLocalCoVar, mkUserLocalOrCoVar,
+        mkDerivedLocalCoVarM,
         mkTemplateLocals, mkTemplateLocalsNum, mkTemplateLocal,
-        mkWorkerId, mkWiredInIdName,
+        mkWorkerId,
 
         -- ** Taking an Id apart
         idName, idType, idUnique, idInfo, idDetails, idRepArity,
@@ -111,7 +114,7 @@ import IdInfo
 import BasicTypes
 
 -- Imported and re-exported
-import Var( Id, DictId,
+import Var( Id, CoVar, DictId,
             idInfo, idDetails, globaliseId, varType,
             isId, isLocalId, isGlobalId, isExportedId )
 import qualified Var
@@ -191,7 +194,7 @@ localiseId id
   | ASSERT( isId id ) isLocalId id && isInternalName name
   = id
   | otherwise
-  = mkLocalIdWithInfo (localiseName name) (idType id) (idInfo id)
+  = Var.mkLocalVar (idDetails id) (localiseName name) (idType id) (idInfo id)
   where
     name = idName id
 
@@ -249,7 +252,31 @@ mkVanillaGlobalWithInfo = mkGlobalId VanillaId
 mkLocalId :: Name -> Type -> Id
 mkLocalId name ty = mkLocalIdWithInfo name ty
                          (vanillaIdInfo `setOneShotInfo` typeOneShot ty)
+ -- It's tempting to ASSERT( not (isCoercionType ty) ), but don't. Sometimes,
+ -- the type is a panic. (Search invented_id)
+
+-- | Make a local CoVar
+mkLocalCoVar :: Name -> Type -> CoVar
+mkLocalCoVar name ty
+  = ASSERT( isCoercionType ty )
+    Var.mkLocalVar CoVarId name ty (vanillaIdInfo `setOneShotInfo` typeOneShot ty)
+
+-- | Like 'mkLocalId', but checks the type to see if it should make a covar
+mkLocalIdOrCoVar :: Name -> Type -> Id
+mkLocalIdOrCoVar name ty
+  | isCoercionType ty = mkLocalCoVar name ty
+  | otherwise         = mkLocalId    name ty
+
+-- | Make a local id, with the IdDetails set to CoVarId if the type indicates
+-- so.
+mkLocalIdOrCoVarWithInfo :: Name -> Type -> IdInfo -> Id
+mkLocalIdOrCoVarWithInfo name ty info
+  = Var.mkLocalVar details name ty info
+  where
+    details | isCoercionType ty = CoVarId
+            | otherwise         = VanillaId
 
+    -- proper ids only; no covars!
 mkLocalIdWithInfo :: Name -> Type -> IdInfo -> Id
 mkLocalIdWithInfo name ty info = Var.mkLocalVar VanillaId name ty info
         -- Note [Free type variables]
@@ -265,26 +292,45 @@ mkExportedLocalId details name ty = Var.mkExportedLocalVar details name ty vanil
 -- | Create a system local 'Id'. These are local 'Id's (see "Var#globalvslocal")
 -- that are created by the compiler out of thin air
 mkSysLocal :: FastString -> Unique -> Type -> Id
-mkSysLocal fs uniq ty = mkLocalId (mkSystemVarName uniq fs) ty
+mkSysLocal fs uniq ty = ASSERT( not (isCoercionType ty) )
+                        mkLocalId (mkSystemVarName uniq fs) ty
+
+-- | Like 'mkSysLocal', but checks to see if we have a covar type
+mkSysLocalOrCoVar :: FastString -> Unique -> Type -> Id
+mkSysLocalOrCoVar fs uniq ty
+  | isCoercionType ty = mkLocalCoVar name ty
+  | otherwise         = mkLocalId    name ty
+  where
+    name = mkSystemVarName uniq fs
 
 mkSysLocalM :: MonadUnique m => FastString -> Type -> m Id
 mkSysLocalM fs ty = getUniqueM >>= (\uniq -> return (mkSysLocal fs uniq ty))
 
+mkSysLocalOrCoVarM :: MonadUnique m => FastString -> Type -> m Id
+mkSysLocalOrCoVarM fs ty
+  = getUniqueM >>= (\uniq -> return (mkSysLocalOrCoVar fs uniq ty))
 
 -- | Create a user local 'Id'. These are local 'Id's (see "Var#globalvslocal") with a name and location that the user might recognize
 mkUserLocal :: OccName -> Unique -> Type -> SrcSpan -> Id
-mkUserLocal occ uniq ty loc = mkLocalId (mkInternalName uniq occ loc) ty
-
-mkUserLocalM :: MonadUnique m => OccName -> Type -> SrcSpan -> m Id
-mkUserLocalM occ ty loc = getUniqueM >>= (\uniq -> return (mkUserLocal occ uniq ty loc))
-
-mkDerivedLocalM :: MonadUnique m => (OccName -> OccName) -> Id -> Type -> m Id
-mkDerivedLocalM deriv_name id ty
-    = getUniqueM >>= (\uniq -> return (mkLocalId (mkDerivedInternalName deriv_name uniq (getName id)) ty))
-
-mkWiredInIdName :: Module -> FastString -> Unique -> Id -> Name
-mkWiredInIdName mod fs uniq id
- = mkWiredInName mod (mkOccNameFS varName fs) uniq (AnId id) UserSyntax
+mkUserLocal occ uniq ty loc = ASSERT( not (isCoercionType ty) )
+                              mkLocalId (mkInternalName uniq occ loc) ty
+
+-- | Like 'mkUserLocal' for covars
+mkUserLocalCoVar :: OccName -> Unique -> Type -> SrcSpan -> Id
+mkUserLocalCoVar occ uniq ty loc
+  = mkLocalCoVar (mkInternalName uniq occ loc) ty
+
+-- | Like 'mkUserLocal', but checks if we have a coercion type
+mkUserLocalOrCoVar :: OccName -> Unique -> Type -> SrcSpan -> Id
+mkUserLocalOrCoVar occ uniq ty loc
+  = mkLocalIdOrCoVar (mkInternalName uniq occ loc) ty
+
+mkDerivedLocalCoVarM :: MonadUnique m => (OccName -> OccName) -> Id -> Type -> m Id
+mkDerivedLocalCoVarM deriv_name id ty
+    = ASSERT( isCoercionType ty )
+      do { uniq <- getUniqueM
+         ; let name = mkDerivedInternalName deriv_name uniq (getName id)
+         ; return (mkLocalCoVar name ty) }
 
 {-
 Make some local @Ids@ for a template @CoreExpr@.  These have bogus
@@ -295,11 +341,11 @@ instantiated before use.
 -- | Workers get local names. "CoreTidy" will externalise these if necessary
 mkWorkerId :: Unique -> Id -> Type -> Id
 mkWorkerId uniq unwrkr ty
-  = mkLocalId (mkDerivedInternalName mkWorkerOcc uniq (getName unwrkr)) ty
+  = mkLocalIdOrCoVar (mkDerivedInternalName mkWorkerOcc uniq (getName unwrkr)) ty
 
 -- | Create a /template local/: a family of system local 'Id's in bijection with @Int@s, typically used in unfoldings
 mkTemplateLocal :: Int -> Type -> Id
-mkTemplateLocal i ty = mkSysLocal (fsLit "tpl") (mkBuiltinUnique i) ty
+mkTemplateLocal i ty = mkSysLocalOrCoVar (fsLit "tpl") (mkBuiltinUnique i) ty
 
 -- | Create a template local for a series of types
 mkTemplateLocals :: [Type] -> [Id]
index 6f00df5..450644d 100644 (file)
@@ -10,7 +10,7 @@ Haskell. [WDP 94/11])
 
 module IdInfo (
         -- * The IdDetails type
-        IdDetails(..), pprIdDetails, coVarDetails,
+        IdDetails(..), pprIdDetails, coVarDetails, isCoVarDetails,
         RecSelParent(..),
 
         -- * The IdInfo type
@@ -135,20 +135,19 @@ data IdDetails
        --                  implemented with a newtype, so it might be bad
        --                  to be strict on this dictionary
 
+  | CoVarId                    -- ^ A coercion variable
+
   -- The rest are distinguished only for debugging reasons
   -- e.g. to suppress them in -ddump-types
   -- Currently we don't persist these through interface file
   -- (see MkIface.toIfaceIdDetails), but we easily could if it mattered
 
-  | DefMethId                   -- ^ A default-method Id, either polymorphic or generic
-
   | ReflectionId                -- ^ A top-level Id to support runtime reflection
                                 -- e.g. $trModule, or $tcT
 
   | PatSynId                    -- ^ A top-level Id to support pattern synonyms;
                                 -- the builder or matcher for the patern synonym
 
-
 data RecSelParent = RecSelData TyCon | RecSelPatSyn PatSyn deriving Eq
   -- Either `TyCon` or `PatSyn` depending
   -- on the origin of the record selector.
@@ -160,10 +159,15 @@ instance Outputable RecSelParent where
             RecSelData ty_con -> ppr ty_con
             RecSelPatSyn ps   -> ppr ps
 
-
-
+-- | Just a synonym for 'CoVarId'. Written separately so it can be
+-- exported in the hs-boot file.
 coVarDetails :: IdDetails
-coVarDetails = VanillaId
+coVarDetails = CoVarId
+
+-- | Check if an 'IdDetails' says 'CoVarId'.
+isCoVarDetails :: IdDetails -> Bool
+isCoVarDetails CoVarId = True
+isCoVarDetails _       = False
 
 instance Outputable IdDetails where
     ppr = pprIdDetails
@@ -173,7 +177,6 @@ pprIdDetails VanillaId = empty
 pprIdDetails other     = brackets (pp other)
  where
    pp VanillaId         = panic "pprIdDetails"
-   pp DefMethId         = ptext (sLit "DefMethId")
    pp ReflectionId      = ptext (sLit "ReflectionId")
    pp PatSynId          = ptext (sLit "PatSynId")
    pp (DataConWorkId _) = ptext (sLit "DataCon")
@@ -186,6 +189,7 @@ pprIdDetails other     = brackets (pp other)
    pp (RecSelId { sel_naughty = is_naughty })
                          = brackets $ ptext (sLit "RecSel")
                             <> ppWhen is_naughty (ptext (sLit "(naughty)"))
+   pp CoVarId           = ptext (sLit "CoVarId")
 
 {-
 ************************************************************************
index 2e98629..0fabad3 100644 (file)
@@ -5,4 +5,6 @@ data IdDetails
 
 vanillaIdInfo :: IdInfo
 coVarDetails :: IdDetails
+isCoVarDetails :: IdDetails -> Bool
 pprIdDetails :: IdDetails -> SDoc
+
index bce3061..4b1fe94 100644 (file)
@@ -226,7 +226,6 @@ okSymChar c
       OtherSymbol          -> True
       _                    -> False
 
-
 -- | All reserved identifiers. Taken from section 2.4 of the 2010 Report.
 reservedIds :: Set.Set String
 reservedIds = Set.fromList [ "case", "class", "data", "default", "deriving"
index 8223f33..b0ef583 100644 (file)
@@ -21,8 +21,7 @@ module MkId (
 
         wrapNewTypeBody, unwrapNewTypeBody,
         wrapFamInstBody, unwrapFamInstScrut,
-        wrapTypeFamInstBody, wrapTypeUnbranchedFamInstBody, unwrapTypeFamInstScrut,
-        unwrapTypeUnbranchedFamInstScrut,
+        wrapTypeUnbranchedFamInstBody, unwrapTypeUnbranchedFamInstScrut,
 
         DataConBoxer(..), mkDataConRep, mkDataConWorkId,
 
@@ -281,8 +280,8 @@ mkDictSelId name clas
     arg_tys        = dataConRepArgTys data_con  -- Includes the dictionary superclasses
     val_index      = assoc "MkId.mkDictSelId" (sel_names `zip` [0..]) name
 
-    sel_ty = mkForAllTys tyvars (mkFunTy (mkClassPred clas (mkTyVarTys tyvars))
-                                         (getNth arg_tys val_index))
+    sel_ty = mkInvForAllTys tyvars (mkFunTy (mkClassPred clas (mkTyVarTys tyvars))
+                                            (getNth arg_tys val_index))
 
     base_info = noCafIdInfo
                 `setArityInfo`         1
@@ -338,7 +337,7 @@ mkDictSelRhs clas val_index
     dict_id        = mkTemplateLocal 1 pred
     arg_ids        = mkTemplateLocalsNum 2 arg_tys
 
-    rhs_body | new_tycon = unwrapNewTypeBody tycon (map mkTyVarTy tyvars) (Var dict_id)
+    rhs_body | new_tycon = unwrapNewTypeBody tycon (mkTyVarTys tyvars) (Var dict_id)
              | otherwise = Case (Var dict_id) dict_id (idType the_arg_id)
                                 [(DataAlt data_con, arg_ids, varToCoreExpr the_arg_id)]
                                 -- varToCoreExpr needed for equality superclass selectors
@@ -458,7 +457,7 @@ dataConCPR con
 type Unboxer = Var -> UniqSM ([Var], CoreExpr -> CoreExpr)
   -- Unbox: bind rep vars by decomposing src var
 
-data Boxer = UnitBox | Boxer (TvSubst -> UniqSM ([Var], CoreExpr))
+data Boxer = UnitBox | Boxer (TCvSubst -> UniqSM ([Var], CoreExpr))
   -- Box:   build src arg using these rep vars
 
 newtype DataConBoxer = DCB ([Type] -> [Var] -> UniqSM ([Var], [CoreBind]))
@@ -507,7 +506,7 @@ mkDataConRep dflags fam_envs wrap_name mb_bangs data_con
                  -- we want to see that w is strict in its two arguments
 
              wrap_unf = mkInlineUnfolding (Just wrap_arity) wrap_rhs
-             wrap_tvs = (univ_tvs `minusList` map fst eq_spec) ++ ex_tvs
+             wrap_tvs = (univ_tvs `minusList` map eqSpecTyVar eq_spec) ++ ex_tvs
              wrap_rhs = mkLams wrap_tvs $
                         mkLams wrap_args $
                         wrapFamInstBody tycon res_ty_args $
@@ -520,13 +519,15 @@ mkDataConRep dflags fam_envs wrap_name mb_bangs data_con
                      , dcr_bangs   = arg_ibangs }) }
 
   where
-    (univ_tvs, ex_tvs, eq_spec, theta, orig_arg_tys, _) = dataConFullSig data_con
-    res_ty_args  = substTyVars (mkTopTvSubst eq_spec) univ_tvs
+    (univ_tvs, ex_tvs, eq_spec, theta, orig_arg_tys, _orig_res_ty)
+      = dataConFullSig data_con
+    res_ty_args  = substTyVars (mkTopTCvSubst (map eqSpecPair eq_spec)) univ_tvs
+
     tycon        = dataConTyCon data_con       -- The representation TyCon (not family)
     wrap_ty      = dataConUserType data_con
     ev_tys       = eqSpecPreds eq_spec ++ theta
     all_arg_tys  = ev_tys ++ orig_arg_tys
-    ev_ibangs    = map mk_pred_strict_mark ev_tys
+    ev_ibangs    = map (const HsLazy) ev_tys
     orig_bangs   = dataConSrcBangs data_con
 
     wrap_arg_tys = theta ++ orig_arg_tys
@@ -550,22 +551,21 @@ mkDataConRep dflags fam_envs wrap_name mb_bangs data_con
     wrapper_reqd = not (isNewTyCon tycon)  -- Newtypes have only a worker
                 && (any isBanged (ev_ibangs ++ arg_ibangs)
                       -- Some forcing/unboxing (includes eq_spec)
-                    || isFamInstTyCon tycon) -- Cast result
+                    || isFamInstTyCon tycon  -- Cast result
+                    || (not $ null eq_spec)) -- GADT
 
     initial_wrap_app = Var (dataConWorkId data_con)
-                      `mkTyApps`  res_ty_args
-                      `mkVarApps` ex_tvs
-                      `mkCoApps`  map (mkReflCo Nominal . snd) eq_spec
-                        -- Dont box the eq_spec coercions since they are
-                        -- marked as HsUnpack by mk_dict_strict_mark
+                       `mkTyApps`  res_ty_args
+                       `mkVarApps` ex_tvs
+                       `mkCoApps`  map (mkReflCo Nominal . eqSpecType) eq_spec
 
     mk_boxer :: [Boxer] -> DataConBoxer
     mk_boxer boxers = DCB (\ ty_args src_vars ->
-                      do { let ex_vars = takeList ex_tvs src_vars
-                               subst1 = mkTopTvSubst (univ_tvs `zip` ty_args)
-                               subst2 = extendTvSubstList subst1 ex_tvs
-                                                          (mkTyVarTys ex_vars)
-                         ; (rep_ids, binds) <- go subst2 boxers (dropList ex_tvs src_vars)
+                      do { let (ex_vars, term_vars) = splitAtList ex_tvs src_vars
+                               subst1 = mkTopTCvSubst (univ_tvs `zip` ty_args)
+                               subst2 = extendTCvSubstList subst1 ex_tvs
+                                                           (mkTyVarTys ex_vars)
+                         ; (rep_ids, binds) <- go subst2 boxers term_vars
                          ; return (ex_vars ++ rep_ids, binds) } )
 
     go _ [] src_vars = ASSERT2( null src_vars, ppr data_con ) return ([], [])
@@ -610,7 +610,7 @@ dataConOrigArgTys of the DataCon.
 -------------------------
 newLocal :: Type -> UniqSM Var
 newLocal ty = do { uniq <- getUniqueM
-                 ; return (mkSysLocal (fsLit "dt") uniq ty) }
+                 ; return (mkSysLocalOrCoVar (fsLit "dt") uniq ty) }
 
 -- | Unpack/Strictness decisions from source module
 dataConSrcToImplBang
@@ -694,7 +694,7 @@ wrapCo co rep_ty (unbox_rep, box_rep)  -- co :: arg_ty ~ rep_ty
                          UnitBox -> do { rep_id <- newLocal (TcType.substTy subst rep_ty)
                                        ; return ([rep_id], Var rep_id) }
                          Boxer boxer -> boxer subst
-               ; let sco = substCo (tvCvSubst subst) co
+               ; let sco = substCo subst co
                ; return (rep_ids, rep_expr `Cast` mkSymCo sco) }
 
 ------------------------
@@ -832,24 +832,6 @@ But it's the *argument* type that matters. This is fine:
         data S = MkS S !Int
 because Int is non-recursive.
 
-
-Note [Unpack equality predicates]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-If we have a GADT with a constructor C :: (a~[b]) => b -> T a
-we definitely want that equality predicate *unboxed* so that it
-takes no space at all.  This is easily done: just give it
-an UNPACK pragma. The rest of the unpack/repack code does the
-heavy lifting.  This one line makes every GADT take a word less
-space for each equality predicate, so it's pretty important!
--}
-
-mk_pred_strict_mark :: PredType -> HsImplBang
-mk_pred_strict_mark pred
-  | isEqPred pred = HsUnpack Nothing
-  -- Note [Unpack equality predicates]
-  | otherwise     = HsLazy
-
-{-
 ************************************************************************
 *                                                                      *
         Wrapping and unwrapping newtypes and type families
@@ -881,7 +863,7 @@ wrapNewTypeBody tycon args result_expr
     wrapFamInstBody tycon args $
     mkCast result_expr (mkSymCo co)
   where
-    co = mkUnbranchedAxInstCo Representational (newTyConCo tycon) args
+    co = mkUnbranchedAxInstCo Representational (newTyConCo tycon) args []
 
 -- When unwrapping, we do *not* apply any family coercion, because this will
 -- be done via a CoPat by the type checker.  We have to do it this way as
@@ -891,7 +873,7 @@ wrapNewTypeBody tycon args result_expr
 unwrapNewTypeBody :: TyCon -> [Type] -> CoreExpr -> CoreExpr
 unwrapNewTypeBody tycon args result_expr
   = ASSERT( isNewTyCon tycon )
-    mkCast result_expr (mkUnbranchedAxInstCo Representational (newTyConCo tycon) args)
+    mkCast result_expr (mkUnbranchedAxInstCo Representational (newTyConCo tycon) args [])
 
 -- If the type constructor is a representation type of a data instance, wrap
 -- the expression into a cast adjusting the expression type, which is an
@@ -901,34 +883,36 @@ unwrapNewTypeBody tycon args result_expr
 wrapFamInstBody :: TyCon -> [Type] -> CoreExpr -> CoreExpr
 wrapFamInstBody tycon args body
   | Just co_con <- tyConFamilyCoercion_maybe tycon
-  = mkCast body (mkSymCo (mkUnbranchedAxInstCo Representational co_con args))
+  = mkCast body (mkSymCo (mkUnbranchedAxInstCo Representational co_con args []))
   | otherwise
   = body
 
 -- Same as `wrapFamInstBody`, but for type family instances, which are
 -- represented by a `CoAxiom`, and not a `TyCon`
-wrapTypeFamInstBody :: CoAxiom br -> Int -> [Type] -> CoreExpr -> CoreExpr
-wrapTypeFamInstBody axiom ind args body
-  = mkCast body (mkSymCo (mkAxInstCo Representational axiom ind args))
+wrapTypeFamInstBody :: CoAxiom br -> Int -> [Type] -> [Coercion]
+                    -> CoreExpr -> CoreExpr
+wrapTypeFamInstBody axiom ind args cos body
+  = mkCast body (mkSymCo (mkAxInstCo Representational axiom ind args cos))
 
-wrapTypeUnbranchedFamInstBody :: CoAxiom Unbranched -> [Type] -> CoreExpr
-                              -> CoreExpr
+wrapTypeUnbranchedFamInstBody :: CoAxiom Unbranched -> [Type] -> [Coercion]
+                              -> CoreExpr -> CoreExpr
 wrapTypeUnbranchedFamInstBody axiom
   = wrapTypeFamInstBody axiom 0
 
 unwrapFamInstScrut :: TyCon -> [Type] -> CoreExpr -> CoreExpr
 unwrapFamInstScrut tycon args scrut
   | Just co_con <- tyConFamilyCoercion_maybe tycon
-  = mkCast scrut (mkUnbranchedAxInstCo Representational co_con args) -- data instances only
+  = mkCast scrut (mkUnbranchedAxInstCo Representational co_con args []) -- data instances only
   | otherwise
   = scrut
 
-unwrapTypeFamInstScrut :: CoAxiom br -> Int -> [Type] -> CoreExpr -> CoreExpr
-unwrapTypeFamInstScrut axiom ind args scrut
-  = mkCast scrut (mkAxInstCo Representational axiom ind args)
+unwrapTypeFamInstScrut :: CoAxiom br -> Int -> [Type] -> [Coercion]
+                       -> CoreExpr -> CoreExpr
+unwrapTypeFamInstScrut axiom ind args cos scrut
+  = mkCast scrut (mkAxInstCo Representational axiom ind args cos)
 
-unwrapTypeUnbranchedFamInstScrut :: CoAxiom Unbranched -> [Type] -> CoreExpr
-                                 -> CoreExpr
+unwrapTypeUnbranchedFamInstScrut :: CoAxiom Unbranched -> [Type] -> [Coercion]
+                                 -> CoreExpr -> CoreExpr
 unwrapTypeUnbranchedFamInstScrut axiom
   = unwrapTypeFamInstScrut axiom 0
 
@@ -945,7 +929,7 @@ mkPrimOpId prim_op
   = id
   where
     (tyvars,arg_tys,res_ty, arity, strict_sig) = primOpSig prim_op
-    ty   = mkForAllTys tyvars (mkFunTys arg_tys res_ty)
+    ty   = mkInvForAllTys tyvars (mkFunTys arg_tys res_ty)
     name = mkWiredInName gHC_PRIM (primOpOcc prim_op)
                          (mkPrimOpIdUnique (primOpTag prim_op))
                          (AnId id) UserSyntax
@@ -972,7 +956,7 @@ mkPrimOpId prim_op
 
 mkFCallId :: DynFlags -> Unique -> ForeignCall -> Type -> Id
 mkFCallId dflags uniq fcall ty
-  = ASSERT( isEmptyVarSet (tyVarsOfType ty) )
+  = ASSERT( isEmptyVarSet (tyCoVarsOfType ty) )
     -- A CCallOpId should have no free type variables;
     -- when doing substitutions won't substitute over it
     mkGlobalId (FCallId fcall) name ty info
@@ -987,9 +971,8 @@ mkFCallId dflags uniq fcall ty
            `setArityInfo`         arity
            `setStrictnessInfo`    strict_sig
 
-    (_, tau)        = tcSplitForAllTys ty
-    (arg_tys, _)    = tcSplitFunTys tau
-    arity           = length arg_tys
+    (bndrs, _)        = tcSplitPiTys ty
+    arity             = count isIdLikeBinder bndrs
 
     strict_sig      = mkClosedStrictSig (replicate arity topDmd) topRes
     -- the call does not claim to be strict in its arguments, since they
@@ -1030,7 +1013,7 @@ mkDictFunId dfun_name tvs theta clas tys
 
 mkDictFunTy :: [TyVar] -> ThetaType -> Class -> [Type] -> Type
 mkDictFunTy tvs theta clas tys
- = mkSigmaTy tvs theta (mkClassPred clas tys)
+ = mkInvSigmaTy tvs theta (mkClassPred clas tys)
 
 {-
 ************************************************************************
@@ -1078,11 +1061,11 @@ dollarId = pcMiscPrelId dollarName ty
              (noCafIdInfo `setUnfoldingInfo` unf)
   where
     fun_ty = mkFunTy alphaTy openBetaTy
-    ty     = mkForAllTys [alphaTyVar, openBetaTyVar] $
+    ty     = mkInvForAllTys [levity2TyVar, alphaTyVar, openBetaTyVar] $
              mkFunTy fun_ty fun_ty
     unf    = mkInlineUnfolding (Just 2) rhs
     [f,x]  = mkTemplateLocals [fun_ty, alphaTy]
-    rhs    = mkLams [alphaTyVar, openBetaTyVar, f, x] $
+    rhs    = mkLams [levity2TyVar, alphaTyVar, openBetaTyVar, f, x] $
              App (Var f) (Var x)
 
 ------------------------------------------------
@@ -1092,7 +1075,7 @@ proxyHashId
   = pcMiscPrelId proxyName ty
        (noCafIdInfo `setUnfoldingInfo` evaldUnfolding) -- Note [evaldUnfoldings]
   where
-    ty      = mkForAllTys [kv, tv] (mkProxyPrimTy k t)
+    ty      = mkInvForAllTys [kv, tv] (mkProxyPrimTy k t)
     kv      = kKiVar
     k       = mkTyVarTy kv
     [tv]    = mkTemplateTyVars [k]
@@ -1107,12 +1090,15 @@ unsafeCoerceId
     info = noCafIdInfo `setInlinePragInfo` alwaysInlinePragma
                        `setUnfoldingInfo`  mkCompulsoryUnfolding rhs
 
+    ty  = mkInvForAllTys [ levity1TyVar, levity2TyVar
+                         , openAlphaTyVar, openBetaTyVar ]
+                         (mkFunTy openAlphaTy openBetaTy)
 
-    ty  = mkForAllTys [openAlphaTyVar,openBetaTyVar]
-                      (mkFunTy openAlphaTy openBetaTy)
     [x] = mkTemplateLocals [openAlphaTy]
-    rhs = mkLams [openAlphaTyVar,openBetaTyVar,x] $
-          Cast (Var x) (mkUnsafeCo openAlphaTy openBetaTy)
+    rhs = mkLams [ levity1TyVar, levity2TyVar
+                 , openAlphaTyVar, openBetaTyVar
+                 , x] $
+          Cast (Var x) (mkUnsafeCo Representational openAlphaTy openBetaTy)
 
 ------------------------------------------------
 nullAddrId :: Id
@@ -1138,8 +1124,8 @@ seqId = pcMiscPrelId seqName ty info
                   -- LHS of rules.  That way we can have rules for 'seq';
                   -- see Note [seqId magic]
 
-    ty  = mkForAllTys [alphaTyVar,betaTyVar]
-                      (mkFunTy alphaTy (mkFunTy betaTy betaTy))
+    ty  = mkInvForAllTys [alphaTyVar,betaTyVar]
+                         (mkFunTy alphaTy (mkFunTy betaTy betaTy))
 
     [x,y] = mkTemplateLocals [alphaTy, betaTy]
     rhs = mkLams [alphaTyVar,betaTyVar,x,y] (Case (Var x) x betaTy [(DEFAULT, [], Var y)])
@@ -1171,18 +1157,23 @@ lazyId :: Id    -- See Note [lazyId magic]
 lazyId = pcMiscPrelId lazyIdName ty info
   where
     info = noCafIdInfo
-    ty  = mkForAllTys [alphaTyVar] (mkFunTy alphaTy alphaTy)
+    ty  = mkInvForAllTys [alphaTyVar] (mkFunTy alphaTy alphaTy)
 
 oneShotId :: Id -- See Note [The oneShot function]
 oneShotId = pcMiscPrelId oneShotName ty info
   where
     info = noCafIdInfo `setInlinePragInfo` alwaysInlinePragma
                        `setUnfoldingInfo`  mkCompulsoryUnfolding rhs
-    ty  = mkForAllTys [openAlphaTyVar, openBetaTyVar] (mkFunTy fun_ty fun_ty)
+    ty  = mkInvForAllTys [ levity1TyVar, levity2TyVar
+                         , openAlphaTyVar, openBetaTyVar ]
+                         (mkFunTy fun_ty fun_ty)
     fun_ty = mkFunTy alphaTy betaTy
-    [body, x] = mkTemplateLocals [fun_ty, alphaTy]
+    [body, x] = mkTemplateLocals [fun_ty, openAlphaTy]
     x' = setOneShotLambda x
-    rhs = mkLams [openAlphaTyVar, openBetaTyVar, body, x'] $ Var body `App` Var x
+    rhs = mkLams [ levity1TyVar, levity2TyVar
+                 , openAlphaTyVar, openBetaTyVar
+                 , body, x'] $
+          Var body `App` Var x
 
 runRWId :: Id -- See Note [runRW magic] in this module
 runRWId = pcMiscPrelId runRWName ty info
@@ -1191,19 +1182,20 @@ runRWId = pcMiscPrelId runRWName ty info
     -- State# RealWorld
     stateRW = mkTyConApp statePrimTyCon [realWorldTy]
     -- (# State# RealWorld, o #)
-    ret_ty  = mkTyConApp unboxedPairTyCon [stateRW, openAlphaTy]
+    ret_ty  = mkTupleTy Unboxed [stateRW, openAlphaTy]
     -- State# RealWorld -> (# State# RealWorld, o #)
     arg_ty  = stateRW `mkFunTy` ret_ty
     -- (State# RealWorld -> (# State# RealWorld, o #))
     --   -> (# State# RealWorld, o #)
-    ty      = mkForAllTys [openAlphaTyVar] (arg_ty `mkFunTy` ret_ty)
+    ty      = mkInvForAllTys [levity1TyVar, openAlphaTyVar] $
+              arg_ty `mkFunTy` ret_ty
 
 --------------------------------------------------------------------------------
 magicDictId :: Id  -- See Note [magicDictId magic]
 magicDictId = pcMiscPrelId magicDictName ty info
   where
   info = noCafIdInfo `setInlinePragInfo` neverInlinePragma
-  ty   = mkForAllTys [alphaTyVar] alphaTy
+  ty   = mkInvForAllTys [alphaTyVar] alphaTy
 
 --------------------------------------------------------------------------------
 
@@ -1212,15 +1204,18 @@ coerceId = pcMiscPrelId coerceName ty info
   where
     info = noCafIdInfo `setInlinePragInfo` alwaysInlinePragma
                        `setUnfoldingInfo`  mkCompulsoryUnfolding rhs
-    eqRTy     = mkTyConApp coercibleTyCon  [liftedTypeKind, alphaTy, betaTy]
-    eqRPrimTy = mkTyConApp eqReprPrimTyCon [liftedTypeKind, alphaTy, betaTy]
-    ty        = mkForAllTys [alphaTyVar, betaTyVar] $
+    eqRTy     = mkTyConApp coercibleTyCon [ liftedTypeKind
+                                          , alphaTy, betaTy ]
+    eqRPrimTy = mkTyConApp eqReprPrimTyCon [ liftedTypeKind
+                                           , liftedTypeKind
+                                           , alphaTy, betaTy ]
+    ty        = mkInvForAllTys [alphaTyVar, betaTyVar] $
                 mkFunTys [eqRTy, alphaTy] betaTy
 
     [eqR,x,eq] = mkTemplateLocals [eqRTy, alphaTy, eqRPrimTy]
     rhs = mkLams [alphaTyVar, betaTyVar, eqR, x] $
           mkWildCase (Var eqR) eqRTy betaTy $
-          [(DataAlt coercibleDataCon, [eq], Cast (Var x) (CoVarCo eq))]
+          [(DataAlt coercibleDataCon, [eq], Cast (Var x) (mkCoVarCo eq))]
 
 {-
 Note [dollarId magic]
@@ -1484,7 +1479,7 @@ voidArgId = mkSysLocal (fsLit "void") voidArgIdKey voidPrimTy
 coercionTokenId :: Id         -- :: () ~ ()
 coercionTokenId -- Used to replace Coercion terms when we go to STG
   = pcMiscPrelId coercionTokenName
-                 (mkTyConApp eqPrimTyCon [liftedTypeKind, unitTy, unitTy])
+                 (mkTyConApp eqPrimTyCon [liftedTypeKind, liftedTypeKind, unitTy, unitTy])
                  noCafIdInfo
 
 pcMiscPrelId :: Name -> Type -> IdInfo -> Id
index 69a694b..0a9ac2c 100644 (file)
@@ -1,12 +1,15 @@
 module MkId where
 import Name( Name )
 import Var( Id )
+import Class( Class )
 import {-# SOURCE #-} DataCon( DataCon )
 import {-# SOURCE #-} PrimOp( PrimOp )
 
 data DataConBoxer
 
 mkDataConWorkId :: Name -> DataCon -> Id
+mkDictSelId     :: Name -> Class   -> Id
+
 mkPrimOpId      :: PrimOp -> Id
 
 magicDictId :: Id
index c557889..769b5aa 100644 (file)
@@ -77,8 +77,8 @@ module Name (
         module OccName
     ) where
 
-import {-# SOURCE #-} TypeRep( TyThing )
-import {-# SOURCE #-} PrelNames( liftedTypeKindTyConKey )
+import {-# SOURCE #-} TyCoRep( TyThing )
+import {-# SOURCE #-} PrelNames( starKindTyConKey, unicodeStarKindTyConKey )
 
 import OccName
 import Module
@@ -645,7 +645,7 @@ pprInfixName  n = pprInfixVar (isSymOcc (getOccName n)) (ppr n)
 
 pprPrefixName :: NamedThing a => a -> SDoc
 pprPrefixName thing
- |  name `hasKey` liftedTypeKindTyConKey
+ | name `hasKey` starKindTyConKey || name `hasKey` unicodeStarKindTyConKey
  = ppr name   -- See Note [Special treatment for kind *]
  | otherwise
  = pprPrefixVar (isSymOcc (nameOccName name)) (ppr name)
@@ -661,7 +661,7 @@ an operator, it is really a special case.
 This pprPrefixName stuff is really only used when printing HsSyn,
 which has to be polymorphic in the name type, and hence has to go via
 the overloaded function pprPrefixOcc.  It's easier where we know the
-type being pretty printed; eg the pretty-printing code in TypeRep.
+type being pretty printed; eg the pretty-printing code in TyCoRep.
 
 See Trac #7645, which led to this.
 -}
index 9018bc4..d2641e2 100644 (file)
@@ -12,7 +12,8 @@ module NameEnv (
 
         -- ** Manipulating these environments
         mkNameEnv,
-        emptyNameEnv, unitNameEnv, nameEnvElts, nameEnvUniqueElts,
+        emptyNameEnv, isEmptyNameEnv,
+        unitNameEnv, nameEnvElts, nameEnvUniqueElts,
         extendNameEnv_C, extendNameEnv_Acc, extendNameEnv,
         extendNameEnvList, extendNameEnvList_C,
         foldNameEnv, filterNameEnv, anyNameEnv,
@@ -68,6 +69,7 @@ depAnal get_defs get_uses nodes
 type NameEnv a = UniqFM a       -- Domain is Name
 
 emptyNameEnv       :: NameEnv a
+isEmptyNameEnv     :: NameEnv a -> Bool
 mkNameEnv          :: [(Name,a)] -> NameEnv a
 nameEnvElts        :: NameEnv a -> [a]
 nameEnvUniqueElts  :: NameEnv a -> [(Unique, a)]
@@ -93,6 +95,7 @@ disjointNameEnv    :: NameEnv a -> NameEnv a -> Bool
 
 nameEnvElts x         = eltsUFM x
 emptyNameEnv          = emptyUFM
+isEmptyNameEnv        = isNullUFM
 unitNameEnv x y       = unitUFM x y
 extendNameEnv x y z   = addToUFM x y z
 extendNameEnvList x l = addListToUFM x l
index e299709..9f162d5 100644 (file)
@@ -56,7 +56,6 @@ module OccName (
         mkDataConWrapperOcc, mkWorkerOcc,
         mkMatcherOcc, mkBuilderOcc,
         mkDefaultMethodOcc,
-        mkGenDefMethodOcc,
         mkDerivedTyConOcc, mkNewTyCoOcc, mkClassOpAuxOcc,
         mkCon2TagOcc, mkTag2ConOcc, mkMaxTagOcc,
         mkClassDataConOcc, mkDictOcc, mkIPOcc,
@@ -94,6 +93,7 @@ module OccName (
         extendOccSetList,
         unionOccSets, unionManyOccSets, minusOccSet, elemOccSet, occSetElts,
         foldOccSet, isEmptyOccSet, intersectOccSet, intersectsOccSet,
+        filterOccSet,
 
         -- * Tidying up
         TidyOccEnv, emptyTidyOccEnv, tidyOccName, initTidyOccEnv,
@@ -449,6 +449,7 @@ foldOccSet        :: (OccName -> b -> b) -> b -> OccSet -> b
 isEmptyOccSet     :: OccSet -> Bool
 intersectOccSet   :: OccSet -> OccSet -> OccSet
 intersectsOccSet  :: OccSet -> OccSet -> Bool
+filterOccSet      :: (OccName -> Bool) -> OccSet -> OccSet
 
 emptyOccSet       = emptyUniqSet
 unitOccSet        = unitUniqSet
@@ -464,6 +465,7 @@ foldOccSet        = foldUniqSet
 isEmptyOccSet     = isEmptyUniqSet
 intersectOccSet   = intersectUniqSets
 intersectsOccSet s1 s2 = not (isEmptyOccSet (s1 `intersectOccSet` s2))
+filterOccSet      = filterUniqSet
 
 {-
 ************************************************************************
@@ -582,7 +584,7 @@ isDerivedOccName occ =
 mkDataConWrapperOcc, mkWorkerOcc,
         mkMatcherOcc, mkBuilderOcc,
         mkDefaultMethodOcc,
-        mkGenDefMethodOcc, mkDerivedTyConOcc, mkClassDataConOcc, mkDictOcc,
+        mkDerivedTyConOcc, mkClassDataConOcc, mkDictOcc,
         mkIPOcc, mkSpecOcc, mkForeignExportOcc, mkRepEqOcc,
         mkGenR, mkGen1R, mkGenRCo,
         mkDataTOcc, mkDataCOcc, mkDataConWorkerOcc, mkNewTyCoOcc,
@@ -597,7 +599,6 @@ mkWorkerOcc         = mk_simple_deriv varName  "$w"
 mkMatcherOcc        = mk_simple_deriv varName  "$m"
 mkBuilderOcc        = mk_simple_deriv varName  "$b"
 mkDefaultMethodOcc  = mk_simple_deriv varName  "$dm"
-mkGenDefMethodOcc   = mk_simple_deriv varName  "$gdm"
 mkClassOpAuxOcc     = mk_simple_deriv varName  "$c"
 mkDerivedTyConOcc   = mk_simple_deriv tcName   ":"      -- The : prefix makes sure it classifies as a tycon/datacon
 mkClassDataConOcc   = mk_simple_deriv dataName "D:"     -- We go straight to the "real" data con
index 01e52af..b7aff18 100644 (file)
@@ -25,7 +25,7 @@ module PatSyn (
 #include "HsVersions.h"
 
 import Type
-import TcType( mkSigmaTy )
+import TcType( mkInvSigmaTy )
 import Name
 import Outputable
 import Unique
@@ -80,14 +80,16 @@ data PatSyn
              -- Matcher function.
              -- If Bool is True then prov_theta and arg_tys are empty
              -- and type is
-             --   forall (r :: ?) univ_tvs. req_theta
+             --   forall (v :: Levity) (r :: TYPE v) univ_tvs.
+             --                          req_theta
              --                       => res_ty
              --                       -> (forall ex_tvs. Void# -> r)
              --                       -> (Void# -> r)
              --                       -> r
              --
              -- Otherwise type is
-             --   forall (r :: ?) univ_tvs. req_theta
+             --   forall (v :: Levity) (r :: TYPE v) univ_tvs.
+             --                          req_theta
              --                       => res_ty
              --                       -> (forall ex_tvs. prov_theta => arg_tys -> r)
              --                       -> (Void# -> r)
@@ -326,8 +328,8 @@ patSynType :: PatSyn -> Type
 patSynType (MkPatSyn { psUnivTyVars = univ_tvs, psReqTheta = req_theta
                      , psExTyVars   = ex_tvs,   psProvTheta = prov_theta
                      , psArgs = orig_args, psOrigResTy = orig_res_ty })
-  = mkSigmaTy univ_tvs req_theta $
-    mkSigmaTy ex_tvs prov_theta $
+  = mkInvSigmaTy univ_tvs req_theta $
+    mkInvSigmaTy ex_tvs prov_theta $
     mkFunTys orig_args orig_res_ty
 
 -- | Should the 'PatSyn' be presented infix?
index 0ac4b7a..07f24a5 100644 (file)
@@ -5,7 +5,7 @@ import Data.Data ( Data )
 import Outputable ( Outputable, OutputableBndr )
 import Unique ( Uniquable )
 import BasicTypes (Arity)
-import {-# SOURCE #-} TypeRep (Type)
+import {-# SOURCE #-} TyCoRep (Type)
 import Var (TyVar)
 import Name (Name)
 
index 7733aee..e171e70 100644 (file)
@@ -45,6 +45,7 @@ module SrcLoc (
         interactiveSrcSpan,
         srcLocSpan, realSrcLocSpan,
         combineSrcSpans,
+        srcSpanFirstCharacter,
 
         -- ** Deconstructing SrcSpan
         srcSpanStart, srcSpanEnd,
@@ -342,6 +343,13 @@ combineRealSrcSpans span1 span2
                                   (srcSpanEndLine span2, srcSpanEndCol span2)
     file = srcSpanFile span1
 
+-- | Convert a SrcSpan into one that represents only its first character
+srcSpanFirstCharacter :: SrcSpan -> SrcSpan
+srcSpanFirstCharacter l@(UnhelpfulSpan {}) = l
+srcSpanFirstCharacter (RealSrcSpan span) = RealSrcSpan $ mkRealSrcSpan loc1 loc2
+  where
+    loc1@(SrcLoc f l c) = realSrcSpanStart span
+    loc2 = SrcLoc f l (c+1)
 {-
 ************************************************************************
 *                                                                      *
index 5705c6f..c9c2240 100644 (file)
@@ -23,7 +23,7 @@ module Unique (
         Unique, Uniquable(..),
 
         -- ** Constructors, desctructors and operations on 'Unique's
-        hasKey,
+        hasKey, cmpByUnique,
 
         pprUnique,
 
@@ -46,7 +46,7 @@ module Unique (
         mkCTupleTyConUnique,
         mkPreludeMiscIdUnique, mkPreludeDataConUnique,
         mkPreludeTyConUnique, mkPreludeClassUnique,
-        mkPArrDataConUnique,
+        mkPArrDataConUnique, mkCoVarUnique,
 
         mkVarOccUnique, mkDataOccUnique, mkTvOccUnique, mkTcOccUnique,
         mkRegSingleUnique, mkRegPairUnique, mkRegClassUnique, mkRegSubUnique,
@@ -168,6 +168,9 @@ instance Uniquable FastString where
 instance Uniquable Int where
  getUnique i = mkUniqueGrimily i
 
+cmpByUnique :: Uniquable a => a -> a -> Ordering
+cmpByUnique x y = (getUnique x) `cmpUnique` (getUnique y)
+
 {-
 ************************************************************************
 *                                                                      *
@@ -307,8 +310,10 @@ mkTupleDataConUnique   :: Boxity -> Arity -> Unique
 mkPrimOpIdUnique       :: Int -> Unique
 mkPreludeMiscIdUnique  :: Int -> Unique
 mkPArrDataConUnique    :: Int -> Unique
+mkCoVarUnique          :: Int -> Unique
 
 mkAlphaTyVarUnique   i = mkUnique '1' i
+mkCoVarUnique        i = mkUnique 'g' i
 mkPreludeClassUnique i = mkUnique '2' i
 
 --------------------------------------------------
index 87658b5..f57111f 100644 (file)
@@ -5,7 +5,8 @@
 \section{@Vars@: Variables}
 -}
 
-{-# LANGUAGE CPP, DeriveDataTypeable #-}
+{-# LANGUAGE CPP, DeriveDataTypeable, MultiWayIf #-}
+
 -- |
 -- #name_types#
 -- GHC uses several kinds of name internally:
@@ -19,8 +20,8 @@
 -- * 'Id.Id': see "Id#name_types"
 --
 -- * 'Var.Var' is a synonym for the 'Id.Id' type but it may additionally
---   potentially contain type variables, which have a 'TypeRep.Kind'
---   rather than a 'TypeRep.Type' and only contain some extra
+--   potentially contain type variables, which have a 'TyCoRep.Kind'
+--   rather than a 'TyCoRep.Type' and only contain some extra
 --   details during typechecking.
 --
 --   These 'Var.Var' names may either be global or local, see "Var#globalvslocal"
 module Var (
         -- * The main data type and synonyms
         Var, CoVar, Id, DictId, DFunId, EvVar, EqVar, EvId, IpId,
-        TyVar, TypeVar, KindVar, TKVar,
+        TyVar, TypeVar, KindVar, TKVar, TyCoVar,
 
         -- ** Taking 'Var's apart
         varName, varUnique, varType,
 
         -- ** Modifying 'Var's
-        setVarName, setVarUnique, setVarType,
+        setVarName, setVarUnique, setVarType, updateVarType,
+        updateVarTypeM,
 
         -- ** Constructing, taking apart, modifying 'Id's
         mkGlobalVar, mkLocalVar, mkExportedLocalVar, mkCoVar,
@@ -50,12 +52,12 @@ module Var (
 
         -- ** Predicates
         isId, isTKVar, isTyVar, isTcTyVar,
-        isLocalVar, isLocalId,
+        isLocalVar, isLocalId, isCoVar, isTyCoVar,
         isGlobalId, isExportedId,
         mustHaveLocalBinding,
 
         -- ** Constructing 'TyVar's
-        mkTyVar, mkTcTyVar, mkKindVar,
+        mkTyVar, mkTcTyVar,
 
         -- ** Taking 'TyVar's apart
         tyVarName, tyVarKind, tcTyVarDetails, setTcTyVarDetails,
@@ -68,13 +70,14 @@ module Var (
 
 #include "HsVersions.h"
 
-import {-# SOURCE #-}   TypeRep( Type, Kind, SuperKind )
-import {-# SOURCE #-}   TcType( TcTyVarDetails, pprTcTyVarDetails )
-import {-# SOURCE #-}   IdInfo( IdDetails, IdInfo, coVarDetails, vanillaIdInfo, pprIdDetails )
+import {-# SOURCE #-}   TyCoRep( Type, Kind )
+import {-# SOURCE #-}   TcType( TcTyVarDetails, pprTcTyVarDetails, vanillaSkolemTv )
+import {-# SOURCE #-}   IdInfo( IdDetails, IdInfo, coVarDetails, isCoVarDetails, vanillaIdInfo, pprIdDetails )
 
 import Name hiding (varName)
 import Unique
 import Util
+import DynFlags
 import FastString
 import Outputable
 
@@ -109,16 +112,13 @@ type EqVar  = EvId      -- Boxed equality evidence
 
 type CoVar = Id         -- See Note [Evidence: EvIds and CoVars]
 
+type TyCoVar = Id       -- Type, kind, *or* coercion variable
+
 {-
 Note [Evidence: EvIds and CoVars]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-* An EvId (evidence Id) is a *boxed*, term-level evidence variable
-  (dictionary, implicit parameter, or equality).
-
-* A CoVar (coercion variable) is an *unboxed* term-level evidence variable
-  of type (t1 ~# t2).  So it's the unboxed version of an EqVar.
-
-* Only CoVars can occur in Coercions, EqVars appear in TcCoercions.
+* An EvId (evidence Id) is a term-level evidence variable
+  (dictionary, implicit parameter, or equality). Could be boxed or unboxed.
 
 * DictId, IpId, and EqVar are synonyms when we know what kind of
   evidence we are talking about.  For example, an EqVar has type (t1 ~ t2).
@@ -166,7 +166,8 @@ data Var
         varName        :: !Name,
         realUnique     :: {-# UNPACK #-} !Int,
         varType        :: Kind,
-        tc_tv_details  :: TcTyVarDetails }
+        tc_tv_details  :: TcTyVarDetails
+  }
 
   | Id {
         varName    :: !Name,
@@ -225,7 +226,13 @@ After CoreTidy, top-level LocalIds are turned into GlobalIds
 -}
 
 instance Outputable Var where
-  ppr var = ppr (varName var) <> getPprStyle (ppr_debug var)
+  ppr var = sdocWithDynFlags $ \dflags ->
+            getPprStyle $ \ppr_style ->
+            if |  debugStyle ppr_style && (not (gopt Opt_SuppressVarKinds dflags))
+                 -> parens (ppr (varName var) <+> ppr_debug var ppr_style <+>
+                          dcolon <+> ppr (tyVarKind var))
+               |  otherwise
+                 -> ppr (varName var) <> ppr_debug var ppr_style
 
 ppr_debug :: Var -> PprStyle -> SDoc
 ppr_debug (TyVar {}) sty
@@ -279,6 +286,13 @@ setVarName var new_name
 setVarType :: Id -> Type -> Id
 setVarType id ty = id { varType = ty }
 
+updateVarType :: (Type -> Type) -> Id -> Id
+updateVarType f id = id { varType = f (varType id) }
+
+updateVarTypeM :: Monad m => (Type -> m Type) -> Id -> m Id
+updateVarTypeM f id = do { ty' <- f (varType id)
+                         ; return (id { varType = ty' }) }
+
 {-
 ************************************************************************
 *                                                                      *
@@ -314,7 +328,7 @@ mkTyVar :: Name -> Kind -> TyVar
 mkTyVar name kind = TyVar { varName    = name
                           , realUnique = getKey (nameUnique name)
                           , varType  = kind
-                        }
+                          }
 
 mkTcTyVar :: Name -> Kind -> TcTyVarDetails -> TyVar
 mkTcTyVar name kind details
@@ -327,22 +341,15 @@ mkTcTyVar name kind details
 
 tcTyVarDetails :: TyVar -> TcTyVarDetails
 tcTyVarDetails (TcTyVar { tc_tv_details = details }) = details
-tcTyVarDetails var = pprPanic "tcTyVarDetails" (ppr var)
+tcTyVarDetails (TyVar {})                            = vanillaSkolemTv
+tcTyVarDetails var = pprPanic "tcTyVarDetails" (ppr var <+> dcolon <+> ppr (tyVarKind var))
 
 setTcTyVarDetails :: TyVar -> TcTyVarDetails -> TyVar
 setTcTyVarDetails tv details = tv { tc_tv_details = details }
 
-mkKindVar :: Name -> SuperKind -> KindVar
--- mkKindVar take a SuperKind as argument because we don't have access
--- to superKind here.
-mkKindVar name kind = TyVar
-  { varName    = name
-  , realUnique = getKey (nameUnique name)
-  , varType    = kind }
-
 {-
-************************************************************************
-*                                                                      *
+%************************************************************************
+%*                                                                      *
 \subsection{Ids}
 *                                                                      *
 ************************************************************************
@@ -431,6 +438,12 @@ isId :: Var -> Bool
 isId (Id {}) = True
 isId _       = False
 
+isTyCoVar :: Var -> Bool
+isTyCoVar v = isTyVar v || isCoVar v
+
+isCoVar :: Var -> Bool
+isCoVar v = isId v && isCoVarDetails (id_details v)
+
 isLocalId :: Var -> Bool
 isLocalId (Id { idScope = LocalId _ }) = True
 isLocalId _                            = False
index 8051721..bdc451a 100644 (file)
@@ -5,19 +5,20 @@
 
 module VarEnv (
         -- * Var, Id and TyVar environments (maps)
-        VarEnv, IdEnv, TyVarEnv, CoVarEnv,
+        VarEnv, IdEnv, TyVarEnv, CoVarEnv, TyCoVarEnv,
 
         -- ** Manipulating these environments
-        emptyVarEnv, unitVarEnv, mkVarEnv,
-        elemVarEnv, varEnvElts, varEnvKeys,
-        extendVarEnv, extendVarEnv_C, extendVarEnv_Acc, extendVarEnvList,
+        emptyVarEnv, unitVarEnv, mkVarEnv, mkVarEnv_Directly,
+        elemVarEnv, varEnvElts, varEnvKeys, varEnvToList,
+        extendVarEnv, extendVarEnv_C, extendVarEnv_Acc, extendVarEnv_Directly,
+        extendVarEnvList,
         plusVarEnv, plusVarEnv_C, plusVarEnv_CD, alterVarEnv,
-        delVarEnvList, delVarEnv,
+        delVarEnvList, delVarEnv, delVarEnv_Directly,
         minusVarEnv, intersectsVarEnv,
         lookupVarEnv, lookupVarEnv_NF, lookupWithDefaultVarEnv,
         mapVarEnv, zipVarEnv,
         modifyVarEnv, modifyVarEnv_Directly,
-        isEmptyVarEnv, foldVarEnv,
+        isEmptyVarEnv, foldVarEnv, foldVarEnv_Directly,
         elemVarEnvByKey, lookupVarEnv_Directly,
         filterVarEnv, filterVarEnv_Directly, restrictVarEnv,
         partitionVarEnv,
@@ -44,13 +45,14 @@ module VarEnv (
         RnEnv2,
 
         -- ** Operations on RnEnv2s
-        mkRnEnv2, rnBndr2, rnBndrs2,
+        mkRnEnv2, rnBndr2, rnBndrs2, rnBndr2_var,
         rnOccL, rnOccR, inRnEnvL, inRnEnvR, rnOccL_maybe, rnOccR_maybe,
-        rnBndrL, rnBndrR, nukeRnEnvL, nukeRnEnvR,
+        rnBndrL, rnBndrR, nukeRnEnvL, nukeRnEnvR, rnSwap,
         delBndrL, delBndrR, delBndrsL, delBndrsR,
         addRnInScopeSet,
         rnEtaL, rnEtaR,
         rnInScope, rnInScopeSet, lookupRnInScope,
+        rnEnvL, rnEnvR,
 
         -- * TidyEnv and its operation
         TidyEnv,
@@ -224,6 +226,14 @@ rnInScope x env = x `elemInScopeSet` in_scope env
 rnInScopeSet :: RnEnv2 -> InScopeSet
 rnInScopeSet = in_scope
 
+-- | Retrieve the left mapping
+rnEnvL :: RnEnv2 -> VarEnv Var
+rnEnvL = envL
+
+-- | Retrieve the right mapping
+rnEnvR :: RnEnv2 -> VarEnv Var
+rnEnvR = envR
+
 rnBndrs2 :: RnEnv2 -> [Var] -> [Var] -> RnEnv2
 -- ^ Applies 'rnBndr2' to several variables: the two variable lists must be of equal length
 rnBndrs2 env bsL bsR = foldl2 rnBndr2 env bsL bsR
@@ -233,10 +243,15 @@ rnBndr2 :: RnEnv2 -> Var -> Var -> RnEnv2
 --                       and binder @bR@ in the Right term.
 -- It finds a new binder, @new_b@,
 -- and returns an environment mapping @bL -> new_b@ and @bR -> new_b@
-rnBndr2 (RV2 { envL = envL, envR = envR, in_scope = in_scope }) bL bR
-  = RV2 { envL     = extendVarEnv envL bL new_b   -- See Note
-        , envR     = extendVarEnv envR bR new_b   -- [Rebinding]
-        , in_scope = extendInScopeSet in_scope new_b }
+rnBndr2 env bL bR = fst $ rnBndr2_var env bL bR
+
+rnBndr2_var :: RnEnv2 -> Var -> Var -> (RnEnv2, Var)
+-- ^ Similar to 'rnBndr2' but returns the new variable as well as the
+-- new environment
+rnBndr2_var (RV2 { envL = envL, envR = envR, in_scope = in_scope }) bL bR
+  = (RV2 { envL            = extendVarEnv envL bL new_b   -- See Note
+         , envR            = extendVarEnv envR bR new_b   -- [Rebinding]
+         , in_scope = extendInScopeSet in_scope new_b }, new_b)
   where
         -- Find a new binder not in scope in either term
     new_b | not (bL `elemInScopeSet` in_scope) = bL
@@ -326,6 +341,11 @@ nukeRnEnvL, nukeRnEnvR :: RnEnv2 -> RnEnv2
 nukeRnEnvL env = env { envL = emptyVarEnv }
 nukeRnEnvR env = env { envR = emptyVarEnv }
 
+rnSwap :: RnEnv2 -> RnEnv2
+-- ^ swap the meaning of left and right
+rnSwap (RV2 { envL = envL, envR = envR, in_scope = in_scope })
+  = RV2 { envL = envR, envR = envL, in_scope = in_scope }
+
 {-
 Note [Eta expansion]
 ~~~~~~~~~~~~~~~~~~~~
@@ -364,24 +384,28 @@ emptyTidyEnv = (emptyTidyOccEnv, emptyVarEnv)
 ************************************************************************
 -}
 
-type VarEnv elt   = UniqFM elt
-type IdEnv elt    = VarEnv elt
-type TyVarEnv elt = VarEnv elt
-type CoVarEnv elt = VarEnv elt
+type VarEnv elt     = UniqFM elt
+type IdEnv elt      = VarEnv elt
+type TyVarEnv elt   = VarEnv elt
+type TyCoVarEnv elt = VarEnv elt
+type CoVarEnv elt   = VarEnv elt
 
 emptyVarEnv       :: VarEnv a
 mkVarEnv          :: [(Var, a)] -> VarEnv a
+mkVarEnv_Directly :: [(Unique, a)] -> VarEnv a
 zipVarEnv         :: [Var] -> [a] -> VarEnv a
 unitVarEnv        :: Var -> a -> VarEnv a
 alterVarEnv       :: (Maybe a -> Maybe a) -> VarEnv a -> Var -> VarEnv a
 extendVarEnv      :: VarEnv a -> Var -> a -> VarEnv a
 extendVarEnv_C    :: (a->a->a) -> VarEnv a -> Var -> a -> VarEnv a
 extendVarEnv_Acc  :: (a->b->b) -> (a->b) -> VarEnv b -> Var -> a -> VarEnv b
+extendVarEnv_Directly :: VarEnv a -> Unique -> a -> VarEnv a
 plusVarEnv        :: VarEnv a -> VarEnv a -> VarEnv a
 extendVarEnvList  :: VarEnv a -> [(Var, a)] -> VarEnv a
 
 lookupVarEnv_Directly :: VarEnv a -> Unique -> Maybe a
 filterVarEnv_Directly :: (Unique -> a -> Bool) -> VarEnv a -> VarEnv a
+delVarEnv_Directly    :: VarEnv a -> Unique -> VarEnv a
 partitionVarEnv   :: (a -> Bool) -> VarEnv a -> (VarEnv a, VarEnv a)
 restrictVarEnv    :: VarEnv a -> VarSet -> VarEnv a
 delVarEnvList     :: VarEnv a -> [Var] -> VarEnv a
@@ -394,6 +418,7 @@ mapVarEnv         :: (a -> b) -> VarEnv a -> VarEnv b
 modifyVarEnv      :: (a -> a) -> VarEnv a -> Var -> VarEnv a
 varEnvElts        :: VarEnv a -> [a]
 varEnvKeys        :: VarEnv a -> [Unique]
+varEnvToList      :: VarEnv a -> [(Unique, a)]
 
 isEmptyVarEnv     :: VarEnv a -> Bool
 lookupVarEnv      :: VarEnv a -> Var -> Maybe a
@@ -403,6 +428,7 @@ lookupWithDefaultVarEnv :: VarEnv a -> a -> Var -> a
 elemVarEnv        :: Var -> VarEnv a -> Bool
 elemVarEnvByKey   :: Unique -> VarEnv a -> Bool
 foldVarEnv        :: (a -> b -> b) -> b -> VarEnv a -> b
+foldVarEnv_Directly :: (Unique -> a -> b -> b) -> b -> VarEnv a -> b
 
 elemVarEnv       = elemUFM
 elemVarEnvByKey  = elemUFM_Directly
@@ -410,6 +436,7 @@ alterVarEnv      = alterUFM
 extendVarEnv     = addToUFM
 extendVarEnv_C   = addToUFM_C
 extendVarEnv_Acc = addToUFM_Acc
+extendVarEnv_Directly = addToUFM_Directly
 extendVarEnvList = addListToUFM
 plusVarEnv_C     = plusUFM_C
 plusVarEnv_CD    = plusUFM_CD
@@ -423,14 +450,18 @@ filterVarEnv     = filterUFM
 lookupWithDefaultVarEnv = lookupWithDefaultUFM
 mapVarEnv        = mapUFM
 mkVarEnv         = listToUFM
+mkVarEnv_Directly= listToUFM_Directly
 emptyVarEnv      = emptyUFM
 varEnvElts       = eltsUFM
 varEnvKeys       = keysUFM
+varEnvToList     = ufmToList
 unitVarEnv       = unitUFM
 isEmptyVarEnv    = isNullUFM
 foldVarEnv       = foldUFM
+foldVarEnv_Directly = foldUFM_Directly
 lookupVarEnv_Directly = lookupUFM_Directly
 filterVarEnv_Directly = filterUFM_Directly
+delVarEnv_Directly    = delFromUFM_Directly
 partitionVarEnv       = partitionUFM
 
 restrictVarEnv env vs = filterVarEnv_Directly keep env
index ce6aea6..7966139 100644 (file)
@@ -7,7 +7,7 @@
 
 module VarSet (
         -- * Var, Id and TyVar set types
-        VarSet, IdSet, TyVarSet, CoVarSet,
+        VarSet, IdSet, TyVarSet, CoVarSet, TyCoVarSet,
 
         -- ** Manipulating these sets
         emptyVarSet, unitVarSet, mkVarSet,
@@ -18,11 +18,12 @@ module VarSet (
         isEmptyVarSet, delVarSet, delVarSetList, delVarSetByKey,
         minusVarSet, foldVarSet, filterVarSet,
         transCloVarSet, fixVarSet,
-        lookupVarSet, mapVarSet, sizeVarSet, seqVarSet,
+        lookupVarSet, lookupVarSetByName,
+        mapVarSet, sizeVarSet, seqVarSet,
         elemVarSetByKey, partitionVarSet,
 
         -- * Deterministic Var set types
-        DVarSet, DIdSet, DTyVarSet,
+        DVarSet, DIdSet, DTyVarSet, DTyCoVarSet,
 
         -- ** Manipulating these sets
         emptyDVarSet, unitDVarSet, mkDVarSet,
@@ -39,8 +40,9 @@ module VarSet (
 
 #include "HsVersions.h"
 
-import Var      ( Var, TyVar, CoVar, Id )
+import Var      ( Var, TyVar, CoVar, TyCoVar, Id )
 import Unique
+import Name     ( Name )
 import UniqSet
 import UniqDSet
 import UniqFM( disjointUFM )
@@ -55,6 +57,7 @@ type VarSet       = UniqSet Var
 type IdSet        = UniqSet Id
 type TyVarSet     = UniqSet TyVar
 type CoVarSet     = UniqSet CoVar
+type TyCoVarSet   = UniqSet TyCoVar
 
 emptyVarSet     :: VarSet
 intersectVarSet :: VarSet -> VarSet -> VarSet
@@ -78,6 +81,7 @@ foldVarSet      :: (Var -> a -> a) -> a -> VarSet -> a
 lookupVarSet    :: VarSet -> Var -> Maybe Var
                         -- Returns the set element, which may be
                         -- (==) to the argument, but not the same as
+lookupVarSetByName :: VarSet -> Name -> Maybe Var
 mapVarSet       :: (Var -> Var) -> VarSet -> VarSet
 sizeVarSet      :: VarSet -> Int
 filterVarSet    :: (Var -> Bool) -> VarSet -> VarSet
@@ -110,6 +114,7 @@ isEmptyVarSet   = isEmptyUniqSet
 mkVarSet        = mkUniqSet
 foldVarSet      = foldUniqSet
 lookupVarSet    = lookupUniqSet
+lookupVarSetByName = lookupUniqSet
 mapVarSet       = mapUniqSet
 sizeVarSet      = sizeUniqSet
 filterVarSet    = filterUniqSet
@@ -168,9 +173,10 @@ seqVarSet s = sizeVarSet s `seq` ()
 -- See Note [Deterministic UniqFM] in UniqDFM for explanation why we need
 -- DVarSet.
 
-type DVarSet = UniqDSet Var
-type DIdSet = UniqDSet Id
-type DTyVarSet = UniqDSet TyVar
+type DVarSet     = UniqDSet Var
+type DIdSet      = UniqDSet Id
+type DTyVarSet   = UniqDSet TyVar
+type DTyCoVarSet = UniqDSet TyCoVar
 
 emptyDVarSet :: DVarSet
 emptyDVarSet = emptyUniqDSet
index d0564e6..ea9fe93 100644 (file)
@@ -16,12 +16,12 @@ module Cmm (
 
      -- * Cmm graphs
      CmmReplGraph, GenCmmReplGraph, CmmFwdRewrite, CmmBwdRewrite,
-   
+
      -- * Info Tables
      CmmTopInfo(..), CmmStackInfo(..), CmmInfoTable(..), topInfoTable,
-     ClosureTypeInfo(..), 
+     ClosureTypeInfo(..),
      C_SRT(..), needsSRT,
-     ProfilingInfo(..), ConstrDescription, 
+     ProfilingInfo(..), ConstrDescription,
 
      -- * Statements, expressions and types
      module CmmNode,
@@ -45,8 +45,8 @@ import Data.Word        ( Word8 )
 --  Cmm, GenCmm
 -----------------------------------------------------------------------------
 
--- A CmmProgram is a list of CmmGroups  
--- A CmmGroup is a list of top-level declarations  
+-- A CmmProgram is a list of CmmGroups
+-- A CmmGroup is a list of top-level declarations
 
 -- When object-splitting is on, each group is compiled into a separate
 -- .o file. So typically we put closely related stuff in a CmmGroup.
@@ -150,7 +150,7 @@ data ProfilingInfo
   = NoProfilingInfo
   | ProfilingInfo [Word8] [Word8] -- closure_type, closure_desc
 
--- C_SRT is what StgSyn.SRT gets translated to... 
+-- C_SRT is what StgSyn.SRT gets translated to...
 -- we add a label for the table, and expect only the 'offset/length' form
 
 data C_SRT = NoC_SRT
index 8a86bb4..4b3897f 100644 (file)
@@ -430,10 +430,10 @@ data GlobalReg
   | XmmReg                      -- 128-bit SIMD vector register
         {-# UNPACK #-} !Int     -- its number
 
-  | YmmReg                      -- 256-bit SIMD vector register 
+  | YmmReg                      -- 256-bit SIMD vector register
         {-# UNPACK #-} !Int     -- its number
 
-  | ZmmReg                      -- 512-bit SIMD vector register 
+  | ZmmReg                      -- 512-bit SIMD vector register
         {-# UNPACK #-} !Int     -- its number
 
   -- STG registers
index 2c332a5..53cfd11 100644 (file)
@@ -851,17 +851,17 @@ areaToSp dflags sp_old _sp_hwm area_off (CmmStackSlot area n)
   = cmmOffset dflags (CmmReg spReg) (sp_old - area_off area - n)
     -- Replace (CmmStackSlot area n) with an offset from Sp
 
-areaToSp dflags _ sp_hwm _ (CmmLit CmmHighStackMark) 
+areaToSp dflags _ sp_hwm _ (CmmLit CmmHighStackMark)
   = mkIntExpr dflags sp_hwm
-    -- Replace CmmHighStackMark with the number of bytes of stack used, 
+    -- Replace CmmHighStackMark with the number of bytes of stack used,
     -- the sp_hwm.   See Note [Stack usage] in StgCmmHeap
 
-areaToSp dflags _ _ _ (CmmMachOp (MO_U_Lt _)  
+areaToSp dflags _ _ _ (CmmMachOp (MO_U_Lt _)
                           [CmmMachOp (MO_Sub _)
                                   [ CmmRegOff (CmmGlobal Sp) x_off
                                   , CmmLit (CmmInt y_lit _)],
                            CmmReg (CmmGlobal SpLim)])
-  | fromIntegral x_off >= y_lit 
+  | fromIntegral x_off >= y_lit
   = zeroExpr dflags
     -- Replace a stack-overflow test that cannot fail with a no-op
     -- See Note [Always false stack check]
index beaf6bc..1e3adf4 100644 (file)
@@ -131,7 +131,7 @@ arfGraph pass@FwdPass { fp_lattice = lattice,
                         fp_transfer = transfer,
                         fp_rewrite  = rewrite } entries g in_fact = graph g in_fact
   where
-    {- nested type synonyms would be so lovely here 
+    {- nested type synonyms would be so lovely here
     type ARF  thing = forall e x . thing e x -> f        -> m (DG f n e x, Fact x f)
     type ARFX thing = forall e x . thing e x -> Fact e f -> m (DG f n e x, Fact x f)
     -}
@@ -190,7 +190,7 @@ arfGraph pass@FwdPass { fp_lattice = lattice,
 
     -- | Compose fact transformers and concatenate the resulting
     -- rewritten graphs.
-    {-# INLINE cat #-} 
+    {-# INLINE cat #-}
     cat ft1 ft2 f = do { (g1,f1) <- ft1 f
                        ; (g2,f2) <- ft2 f1
                        ; let !g = g1 `dgSplice` g2
@@ -199,7 +199,7 @@ arfGraph pass@FwdPass { fp_lattice = lattice,
     arfx :: forall x .
             (Block n C x ->        f -> UniqSM (DG f n C x, Fact x f))
          -> (Block n C x -> Fact C f -> UniqSM (DG f n C x, Fact x f))
-    arfx arf thing fb = 
+    arfx arf thing fb =
       arf thing $ fromJust $ lookupFact (entryLabel thing) $ joinInFacts lattice fb
      -- joinInFacts adds debugging information
 
@@ -398,14 +398,14 @@ arbGraph pass@BwdPass { bp_lattice  = lattice,
                         bp_transfer = transfer,
                         bp_rewrite  = rewrite } entries g in_fact = graph g in_fact
   where
-    {- nested type synonyms would be so lovely here 
+    {- nested type synonyms would be so lovely here
     type ARB  thing = forall e x . thing e x -> Fact x f -> m (DG f n e x, f)
     type ARBX thing = forall e x . thing e x -> Fact x f -> m (DG f n e x, Fact e f)
     -}
     graph ::              Graph n e x -> Fact x f -> UniqSM (DG f n e x, Fact e f)
     block :: forall e x . Block n e x -> Fact x f -> UniqSM (DG f n e x, f)
     body  :: [Label] -> Body n -> Fact C f -> UniqSM (DG f n C C, Fact C f)
-    node  :: forall e x . (ShapeLifter e x) 
+    node  :: forall e x . (ShapeLifter e x)
              => n e x       -> Fact x f -> UniqSM (DG f n e x, f)
     cat :: forall e a x info info' info''.
            (info' -> UniqSM (DG f n e a, info''))
@@ -450,7 +450,7 @@ arbGraph pass@BwdPass { bp_lattice  = lattice,
 
     -- | Compose fact transformers and concatenate the resulting
     -- rewritten graphs.
-    {-# INLINE cat #-} 
+    {-# INLINE cat #-}
     cat ft1 ft2 f = do { (g2,f2) <- ft2 f
                        ; (g1,f1) <- ft1 f2
                        ; let !g = g1 `dgSplice` g2
@@ -591,7 +591,7 @@ fixpoint direction DataflowLattice{ fact_bot = _, fact_join = join }
 
            let newblocks' = case rg of
                               GMany _ blks _ -> mapUnion blks newblocks
-     
+
            loop todo' fbase' newblocks'
 
 
@@ -633,7 +633,7 @@ iteration.
 Note [Unreachable blocks]
 ~~~~~~~~~~~~~~~~~~~~~~~~~
 A block that is not in the domain of tfb_fbase is "currently unreachable".
-A currently-unreachable block is not even analyzed.  Reason: consider 
+A currently-unreachable block is not even analyzed.  Reason: consider
 constant prop and this graph, with entry point L1:
   L1: x:=3; goto L4
   L2: x:=4; goto L4
@@ -849,7 +849,7 @@ getFact lat l fb = case lookupFact l fb of Just  f -> f
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 -}
 -- $fuel
--- A value of type 'FwdRewrite' or 'BwdRewrite' /respects fuel/ if 
+-- A value of type 'FwdRewrite' or 'BwdRewrite' /respects fuel/ if
 -- any function contained within the value satisfies the following properties:
 --
 --   * When fuel is exhausted, it always returns 'Nothing'.
@@ -857,7 +857,7 @@ getFact lat l fb = case lookupFact l fb of Just  f -> f
 --   * When it returns @Just g rw@, it consumes /exactly/ one unit
 --     of fuel, and new rewrite 'rw' also respects fuel.
 --
--- Provided that functions passed to 'mkFRewrite', 'mkFRewrite3', 
+-- Provided that functions passed to 'mkFRewrite', 'mkFRewrite3',
 -- 'mkBRewrite', and 'mkBRewrite3' are not aware of the fuel supply,
 -- the results respect fuel.
 --
index f5a722e..d10903d 100644 (file)
@@ -77,7 +77,7 @@ import DataCon
 import FastString
 import Name
 import Type
-import TypeRep
+import TyCoRep
 import TcType
 import TyCon
 import BasicTypes
@@ -957,16 +957,18 @@ getTyDescription :: Type -> String
 getTyDescription ty
   = case (tcSplitSigmaTy ty) of { (_, _, tau_ty) ->
     case tau_ty of
-      TyVarTy _                            -> "*"
-      AppTy fun _                   -> getTyDescription fun
-      FunTy _ res                   -> '-' : '>' : fun_result res
-      TyConApp tycon _              -> getOccString tycon
-      ForAllTy _ ty          -> getTyDescription ty
+      TyVarTy _              -> "*"
+      AppTy fun _            -> getTyDescription fun
+      TyConApp tycon _       -> getOccString tycon
+      ForAllTy (Anon _) res  -> '-' : '>' : fun_result res
+      ForAllTy (Named {}) ty -> getTyDescription ty
       LitTy n                -> getTyLitDescription n
+      CastTy ty _            -> getTyDescription ty
+      CoercionTy co          -> pprPanic "getTyDescription" (ppr co)
     }
   where
-    fun_result (FunTy _ res) = '>' : fun_result res
-    fun_result other             = getTyDescription other
+    fun_result (ForAllTy (Anon _) res) = '>' : fun_result res
+    fun_result other                   = getTyDescription other
 
 getTyLitDescription :: TyLit -> String
 getTyLitDescription l =
index 03c11cc..b46ab5a 100644 (file)
@@ -17,7 +17,7 @@ module StgCmmLayout (
 
         slowCall, directCall,
 
-        mkVirtHeapOffsets, mkVirtConstrOffsets, getHpRelOffset, 
+        mkVirtHeapOffsets, mkVirtConstrOffsets, getHpRelOffset,
 
         ArgRep(..), toArgRep, argRepSizeW -- re-exported from StgCmmArgRep
   ) where
index 30bc962..e832f54 100644 (file)
@@ -106,11 +106,10 @@ typeArity ty
   = go initRecTc ty
   where
     go rec_nts ty
-      | Just (_, ty')  <- splitForAllTy_maybe ty
-      = go rec_nts ty'
-
-      | Just (arg,res) <- splitFunTy_maybe ty
-      = typeOneShot arg : go rec_nts res
+      | Just (bndr, ty')  <- splitPiTy_maybe ty
+      = if isIdLikeBinder bndr
+        then typeOneShot (binderType bndr) : go rec_nts ty'
+        else go rec_nts ty'
 
       | Just (tc,tys) <- splitTyConApp_maybe ty
       , Just (ty', _) <- instNewTyCon_maybe tc tys
@@ -771,11 +770,11 @@ arityType env (Tick t e)
 arityType _ _ = vanillaArityType
 
 {-
-************************************************************************
-*                                                                      *
+%************************************************************************
+%*                                                                      *
               The main eta-expander
-*                                                                      *
-************************************************************************
+%*                                                                      *
+%************************************************************************
 
 We go for:
    f = \x1..xn -> N  ==>   f = \x1..xn y1..ym -> N y1..ym
@@ -964,21 +963,19 @@ mkEtaWW :: Arity -> CoreExpr -> InScopeSet -> Type
 mkEtaWW orig_n orig_expr in_scope orig_ty
   = go orig_n empty_subst orig_ty []
   where
-    empty_subst = TvSubst in_scope emptyTvSubstEnv
+    empty_subst = mkEmptyTCvSubst in_scope
 
     go n subst ty eis       -- See Note [exprArity invariant]
        | n == 0
-       = (getTvInScope subst, reverse eis)
-
-       | Just (tv,ty') <- splitForAllTy_maybe ty
-       , let (subst', tv') = Type.substTyVarBndr subst tv
-           -- Avoid free vars of the original expression
-       = go n subst' ty' (EtaVar tv' : eis)
+       = (getTCvInScope subst, reverse eis)
 
-       | Just (arg_ty, res_ty) <- splitFunTy_maybe ty
-       , let (subst', eta_id') = freshEtaId n subst arg_ty
-           -- Avoid free vars of the original expression
-       = go (n-1) subst' res_ty (EtaVar eta_id' : eis)
+       | Just (bndr,ty') <- splitPiTy_maybe ty
+       = let ((subst', eta_id'), new_n) = caseBinder bndr
+               (\tv -> (Type.substTyVarBndr subst tv, n))
+               (\arg_ty -> (freshEtaVar n subst arg_ty, n-1))
+         in
+            -- Avoid free vars of the original expression
+         go new_n subst' ty' (EtaVar eta_id' : eis)
 
        | Just (co, ty') <- topNormaliseNewType_maybe ty
        =        -- Given this:
@@ -992,7 +989,7 @@ mkEtaWW orig_n orig_expr in_scope orig_ty
        | otherwise       -- We have an expression of arity > 0,
                          -- but its type isn't a function.
        = WARN( True, (ppr orig_n <+> ppr orig_ty) $$ ppr orig_expr )
-         (getTvInScope subst, reverse eis)
+         (getTCvInScope subst, reverse eis)
         -- This *can* legitmately happen:
         -- e.g.  coerce Int (\x. x) Essentially the programmer is
         -- playing fast and loose with types (Happy does this a lot).
@@ -1011,7 +1008,7 @@ subst_bind = substBindSC
 
 
 --------------
-freshEtaId :: Int -> TvSubst -> Type -> (TvSubst, Id)
+freshEtaVar :: Int -> TCvSubst -> Type -> (TCvSubst, Var)
 -- Make a fresh Id, with specified type (after applying substitution)
 -- It should be "fresh" in the sense that it's not in the in-scope set
 -- of the TvSubstEnv; and it should itself then be added to the in-scope
@@ -1019,10 +1016,10 @@ freshEtaId :: Int -> TvSubst -> Type -> (TvSubst, Id)
 --
 -- The Int is just a reasonable starting point for generating a unique;
 -- it does not necessarily have to be unique itself.
-freshEtaId n subst ty
+freshEtaVar n subst ty
       = (subst', eta_id')
       where
         ty'     = Type.substTy subst ty
-        eta_id' = uniqAway (getTvInScope subst) $
-                  mkSysLocal (fsLit "eta") (mkBuiltinUnique n) ty'
-        subst'  = extendTvInScope subst eta_id'
+        eta_id' = uniqAway (getTCvInScope subst) $
+                  mkSysLocalOrCoVar (fsLit "eta") (mkBuiltinUnique n) ty'
+        subst'  = extendTCvInScope subst eta_id'
index 398f6be..bf5d773 100644 (file)
@@ -22,9 +22,10 @@ module CoreFVs (
         exprSomeFreeVars, exprsSomeFreeVars,
 
         -- * Free variables of Rules, Vars and Ids
-        varTypeTyVars,
-        varTypeTyVarsAcc,
-        idUnfoldingVars, idFreeVars, idRuleAndUnfoldingVars,
+        varTypeTyCoVars,
+        varTypeTyCoVarsAcc,
+        idUnfoldingVars, idFreeVars, dIdFreeVars,
+        idRuleAndUnfoldingVars, idRuleAndUnfoldingVarsDSet,
         idFreeVarsAcc,
         idRuleVars, idRuleRhsVars, stableUnfoldingVars,
         ruleRhsFreeVars, ruleFreeVars, rulesFreeVars,
@@ -35,10 +36,16 @@ module CoreFVs (
         expr_fvs,
 
         -- * Core syntax tree annotation with free variables
-        CoreExprWithFVs,        -- = AnnExpr Id DVarSet
-        CoreBindWithFVs,        -- = AnnBind Id DVarSet
+        FVAnn,                  -- annotation, abstract
+        CoreExprWithFVs,        -- = AnnExpr Id FVAnn
+        CoreExprWithFVs',       -- = AnnExpr' Id FVAnn
+        CoreBindWithFVs,        -- = AnnBind Id FVAnn
+        CoreAltWithFVs,         -- = AnnAlt Id FVAnn
         freeVars,               -- CoreExpr -> CoreExprWithFVs
-        freeVarsOf              -- CoreExprWithFVs -> DIdSet
+        freeVarsOf,             -- CoreExprWithFVs -> DIdSet
+        freeVarsOfType,         -- CoreExprWithFVs -> TyCoVarSet
+        freeVarsOfAnn, freeVarsOfTypeAnn,
+        exprTypeFV              -- CoreExprWithFVs -> Type
     ) where
 
 #include "HsVersions.h"
@@ -48,10 +55,12 @@ import Id
 import IdInfo
 import NameSet
 import UniqFM
+import Literal ( literalType )
 import Name
 import VarSet
 import Var
 import TcType
+import Type
 import Coercion
 import Maybes( orElse )
 import Util
@@ -161,7 +170,7 @@ exprsSomeFreeVars fv_cand es =
 
 addBndr :: CoreBndr -> FV -> FV
 addBndr bndr fv fv_cand in_scope acc
-  = (varTypeTyVarsAcc bndr `unionFV`
+  = (varTypeTyCoVarsAcc bndr `unionFV`
         -- Include type varibles in the binder's type
         --      (not just Ids; coercion variables too!)
      FV.delFV bndr fv) fv_cand in_scope acc
@@ -171,7 +180,7 @@ addBndrs bndrs fv = foldr addBndr fv bndrs
 
 expr_fvs :: CoreExpr -> FV
 expr_fvs (Type ty) fv_cand in_scope acc =
-  tyVarsOfTypeAcc ty fv_cand in_scope acc
+  tyCoVarsOfTypeAcc ty fv_cand in_scope acc
 expr_fvs (Coercion co) fv_cand in_scope acc =
   tyCoVarsOfCoAcc co fv_cand in_scope acc
 expr_fvs (Var var) fv_cand in_scope acc = oneVar var fv_cand in_scope acc
@@ -186,7 +195,7 @@ expr_fvs (Cast expr co) fv_cand in_scope acc =
   (expr_fvs expr `unionFV` tyCoVarsOfCoAcc co) fv_cand in_scope acc
 
 expr_fvs (Case scrut bndr ty alts) fv_cand in_scope acc
-  = (expr_fvs scrut `unionFV` tyVarsOfTypeAcc ty `unionFV` addBndr bndr
+  = (expr_fvs scrut `unionFV` tyCoVarsOfTypeAcc ty `unionFV` addBndr bndr
       (mapUnionFV alt_fvs alts)) fv_cand in_scope acc
   where
     alt_fvs (_, bndrs, rhs) = addBndrs bndrs (expr_fvs rhs)
@@ -353,16 +362,42 @@ The free variable pass annotates every node in the expression with its
 NON-GLOBAL free variables and type variables.
 -}
 
+data FVAnn = FVAnn { fva_fvs    :: DVarSet   -- free in expression
+                   , fva_ty_fvs :: DVarSet   -- free only in expression's type
+                   , fva_ty     :: Type      -- expression's type
+                   }
+
 -- | Every node in a binding group annotated with its
--- (non-global) free variables, both Ids and TyVars
-type CoreBindWithFVs = AnnBind Id DVarSet
+-- (non-global) free variables, both Ids and TyVars, and type.
+type CoreBindWithFVs = AnnBind Id FVAnn
+-- | Every node in an expression annotated with its
+-- (non-global) free variables, both Ids and TyVars, and type.
+type CoreExprWithFVs  = AnnExpr Id FVAnn
+type CoreExprWithFVs' = AnnExpr' Id FVAnn
+
 -- | Every node in an expression annotated with its
--- (non-global) free variables, both Ids and TyVars
-type CoreExprWithFVs = AnnExpr Id DVarSet
+-- (non-global) free variables, both Ids and TyVars, and type.
+type CoreAltWithFVs = AnnAlt Id FVAnn
 
 freeVarsOf :: CoreExprWithFVs -> DIdSet
 -- ^ Inverse function to 'freeVars'
-freeVarsOf (free_vars, _) = free_vars
+freeVarsOf (FVAnn { fva_fvs = fvs }, _) = fvs
+
+-- | Extract the vars free in an annotated expression's type
+freeVarsOfType :: CoreExprWithFVs -> DTyCoVarSet
+freeVarsOfType (FVAnn { fva_ty_fvs = ty_fvs }, _) = ty_fvs
+
+-- | Extract the type of an annotated expression. (This is cheap.)
+exprTypeFV :: CoreExprWithFVs -> Type
+exprTypeFV (FVAnn { fva_ty = ty }, _) = ty
+
+-- | Extract the vars reported in a FVAnn
+freeVarsOfAnn :: FVAnn -> DIdSet
+freeVarsOfAnn = fva_fvs
+
+-- | Extract the type-level vars reported in a FVAnn
+freeVarsOfTypeAnn :: FVAnn -> DTyCoVarSet
+freeVarsOfTypeAnn = fva_ty_fvs
 
 noFVs :: VarSet
 noFVs = emptyVarSet
@@ -373,6 +408,9 @@ aFreeVar = unitDVarSet
 unionFVs :: DVarSet -> DVarSet -> DVarSet
 unionFVs = unionDVarSet
 
+unionFVss :: [DVarSet] -> DVarSet
+unionFVss = unionDVarSets
+
 delBindersFV :: [Var] -> DVarSet -> DVarSet
 delBindersFV bs fvs = foldr delBinderFV fvs bs
 
@@ -407,27 +445,30 @@ delBinderFV :: Var -> DVarSet -> DVarSet
 --                        where
 --                          bottom = bottom -- Never evaluated
 
-delBinderFV b s = (s `delDVarSet` b) `unionFVs` dVarTypeTyVars b
+delBinderFV b s = (s `delDVarSet` b) `unionFVs` dVarTypeTyCoVars b
         -- Include coercion variables too!
 
-varTypeTyVars :: Var -> TyVarSet
+varTypeTyCoVars :: Var -> TyCoVarSet
 -- Find the type/kind variables free in the type of the id/tyvar
-varTypeTyVars var = runFVSet $ varTypeTyVarsAcc var
+varTypeTyCoVars var = runFVSet $ varTypeTyCoVarsAcc var
 
-dVarTypeTyVars :: Var -> DTyVarSet
--- Find the type/kind variables free in the type of the id/tyvar
-dVarTypeTyVars var = runFVDSet $ varTypeTyVarsAcc var
+dVarTypeTyCoVars :: Var -> DTyCoVarSet
+-- Find the type/kind/coercion variables free in the type of the id/tyvar
+dVarTypeTyCoVars var = runFVDSet $ varTypeTyCoVarsAcc var
 
-varTypeTyVarsAcc :: Var -> FV
-varTypeTyVarsAcc var = tyVarsOfTypeAcc (varType var)
+varTypeTyCoVarsAcc :: Var -> FV
+varTypeTyCoVarsAcc var = tyCoVarsOfTypeAcc (varType var)
 
 idFreeVars :: Id -> VarSet
 idFreeVars id = ASSERT( isId id) runFVSet $ idFreeVarsAcc id
 
+dIdFreeVars :: Id -> DVarSet
+dIdFreeVars id = runFVDSet $ idFreeVarsAcc id
+
 idFreeVarsAcc :: Id -> FV
 -- Type variables, rule variables, and inline variables
 idFreeVarsAcc id = ASSERT( isId id)
-                   varTypeTyVarsAcc id `unionFV`
+                   varTypeTyCoVarsAcc id `unionFV`
                    idRuleAndUnfoldingVarsAcc id
 
 bndrRuleAndUnfoldingVarsAcc :: Var -> FV
@@ -437,6 +478,9 @@ bndrRuleAndUnfoldingVarsAcc v | isTyVar v = noVars
 idRuleAndUnfoldingVars :: Id -> VarSet
 idRuleAndUnfoldingVars id = runFVSet $ idRuleAndUnfoldingVarsAcc id
 
+idRuleAndUnfoldingVarsDSet :: Id -> DVarSet
+idRuleAndUnfoldingVarsDSet id = runFVDSet $ idRuleAndUnfoldingVarsAcc id
+
 idRuleAndUnfoldingVarsAcc :: Id -> FV
 idRuleAndUnfoldingVarsAcc id = ASSERT( isId id)
                                idRuleVarsAcc id `unionFV` idUnfoldingVarsAcc id
@@ -485,83 +529,127 @@ stableUnfoldingVarsAcc unf
 
 freeVars :: CoreExpr -> CoreExprWithFVs
 -- ^ Annotate a 'CoreExpr' with its (non-global) free type and value variables at every tree node
-freeVars (Var v)
-  = (fvs, AnnVar v)
-  where
-        -- ToDo: insert motivating example for why we *need*
-        -- to include the idSpecVars in the FV list.
-        --      Actually [June 98] I don't think it's necessary
-        -- fvs = fvs_v `unionVarSet` idSpecVars v
-
-    fvs | isLocalVar v = aFreeVar v
-        | otherwise    = emptyDVarSet
-
-freeVars (Lit lit) = (emptyDVarSet, AnnLit lit)
-freeVars (Lam b body)
-  = (b `delBinderFV` freeVarsOf body', AnnLam b body')
-  where
-    body' = freeVars body
-
-freeVars (App fun arg)
-  = (freeVarsOf fun2 `unionFVs` freeVarsOf arg2, AnnApp fun2 arg2)
-  where
-    fun2 = freeVars fun
-    arg2 = freeVars arg
-
-freeVars (Case scrut bndr ty alts)
-  = ((bndr `delBinderFV` alts_fvs) `unionFVs` freeVarsOf scrut2 `unionFVs` runFVDSet (tyVarsOfTypeAcc ty),
-     AnnCase scrut2 bndr ty alts2)
+freeVars = go
   where
-    scrut2 = freeVars scrut
-
-    (alts_fvs_s, alts2) = mapAndUnzip fv_alt alts
-    alts_fvs            = foldr unionFVs emptyDVarSet alts_fvs_s
-
-    fv_alt (con,args,rhs) = (delBindersFV args (freeVarsOf rhs2),
-                             (con, args, rhs2))
-                          where
-                             rhs2 = freeVars rhs
-
-freeVars (Let (NonRec binder rhs) body)
-  = (freeVarsOf rhs2
-       `unionFVs` body_fvs
-       `unionFVs` runFVDSet (bndrRuleAndUnfoldingVarsAcc binder),
-                -- Remember any rules; cf rhs_fvs above
-     AnnLet (AnnNonRec binder rhs2) body2)
-  where
-    rhs2     = freeVars rhs
-    body2    = freeVars body
-    body_fvs = binder `delBinderFV` freeVarsOf body2
-
-freeVars (Let (Rec binds) body)
-  = (delBindersFV binders all_fvs,
-     AnnLet (AnnRec (binders `zip` rhss2)) body2)
-  where
-    (binders, rhss) = unzip binds
-
-    rhss2     = map freeVars rhss
-    rhs_body_fvs = foldr (unionFVs . freeVarsOf) body_fvs rhss2
-    binders_fvs = runFVDSet $ mapUnionFV idRuleAndUnfoldingVarsAcc binders
-    all_fvs      = rhs_body_fvs `unionFVs` binders_fvs
-        -- The "delBinderFV" happens after adding the idSpecVars,
-        -- since the latter may add some of the binders as fvs
-
-    body2     = freeVars body
-    body_fvs  = freeVarsOf body2
+    go :: CoreExpr -> CoreExprWithFVs
+    go (Var v)
+      = (FVAnn fvs ty_fvs (idType v), AnnVar v)
+      where
+            -- ToDo: insert motivating example for why we *need*
+            -- to include the idSpecVars in the FV list.
+            --      Actually [June 98] I don't think it's necessary
+            -- fvs = fvs_v `unionVarSet` idSpecVars v
+
+        (fvs, ty_fvs)
+            | isLocalVar v = (aFreeVar v `unionFVs` ty_fvs, dVarTypeTyCoVars v)
+            | otherwise    = (emptyDVarSet, emptyDVarSet)
+
+    go (Lit lit) = (FVAnn emptyDVarSet emptyDVarSet (literalType lit), AnnLit lit)
+    go (Lam b body)
+      = ( FVAnn { fva_fvs    = b_fvs `unionFVs` (b `delBinderFV` body_fvs)
+                , fva_ty_fvs = b_fvs `unionFVs` (b `delBinderFV` body_ty_fvs)
+                , fva_ty     = mkFunTy b_ty body_ty }
+        , AnnLam b body' )
+      where
+        body'@(FVAnn { fva_fvs = body_fvs, fva_ty_fvs = body_ty_fvs
+                     , fva_ty = body_ty }, _) = go body
+        b_ty  = idType b
+        b_fvs = tyCoVarsOfTypeDSet b_ty
+
+    go (App fun arg)
+      = ( FVAnn { fva_fvs    = freeVarsOf fun' `unionFVs` freeVarsOf arg'
+                , fva_ty_fvs = tyCoVarsOfTypeDSet res_ty
+                , fva_ty     = res_ty }
+        , AnnApp fun' arg' )
+      where
+        fun'   = go fun
+        fun_ty = exprTypeFV fun'
+        arg'   = go arg
+        res_ty = applyTypeToArg fun_ty arg
+
+    go (Case scrut bndr ty alts)
+      = ( FVAnn { fva_fvs = (bndr `delBinderFV` alts_fvs)
+                            `unionFVs` freeVarsOf scrut2
+                            `unionFVs` tyCoVarsOfTypeDSet ty
+                           -- don't need to look at (idType bndr)
+                           -- b/c that's redundant with scrut
+                , fva_ty_fvs = tyCoVarsOfTypeDSet ty
+                , fva_ty     = ty }
+        , AnnCase scrut2 bndr ty alts2 )
+      where
+        scrut2 = go scrut
+
+        (alts_fvs_s, alts2) = mapAndUnzip fv_alt alts
+        alts_fvs            = unionFVss alts_fvs_s
+
+        fv_alt (con,args,rhs) = (delBindersFV args (freeVarsOf rhs2),
+                                 (con, args, rhs2))
+                              where
+                                 rhs2 = go rhs
+
+    go (Let (NonRec binder rhs) body)
+      = ( FVAnn { fva_fvs    = freeVarsOf rhs2
+                               `unionFVs` body_fvs
+                               `unionFVs` runFVDSet
+                                            (bndrRuleAndUnfoldingVarsAcc binder)
+                               -- Remember any rules; cf rhs_fvs above
+                , fva_ty_fvs = freeVarsOfType body2
+                , fva_ty     = exprTypeFV body2 }
+        , AnnLet (AnnNonRec binder rhs2) body2 )
+      where
+        rhs2     = go rhs
+        body2    = go body
+        body_fvs = binder `delBinderFV` freeVarsOf body2
+
+    go (Let (Rec binds) body)
+      = ( FVAnn { fva_fvs    = delBindersFV binders all_fvs
+                , fva_ty_fvs = freeVarsOfType body2
+                , fva_ty     = exprTypeFV body2 }
+        , AnnLet (AnnRec (binders `zip` rhss2)) body2 )
+      where
+        (binders, rhss) = unzip binds
 
-freeVars (Cast expr co)
-  = (freeVarsOf expr2 `unionFVs` cfvs, AnnCast expr2 (cfvs, co))
-  where
-    expr2 = freeVars expr
-    cfvs  = runFVDSet $ tyCoVarsOfCoAcc co
+        rhss2        = map go rhss
+        rhs_body_fvs = foldr (unionFVs . freeVarsOf) body_fvs rhss2
+        binders_fvs  = runFVDSet $ mapUnionFV idRuleAndUnfoldingVarsAcc binders
+        all_fvs      = rhs_body_fvs `unionFVs` binders_fvs
+            -- The "delBinderFV" happens after adding the idSpecVars,
+            -- since the latter may add some of the binders as fvs
 
-freeVars (Tick tickish expr)
-  = (tickishFVs tickish `unionFVs` freeVarsOf expr2, AnnTick tickish expr2)
-  where
-    expr2 = freeVars expr
-    tickishFVs (Breakpoint _ ids) = mkDVarSet ids
-    tickishFVs _                  = emptyDVarSet
+        body2    = go body
+        body_fvs = freeVarsOf body2
 
-freeVars (Type ty) = (runFVDSet $ tyVarsOfTypeAcc ty, AnnType ty)
+    go (Cast expr co)
+      = ( FVAnn (freeVarsOf expr2 `unionFVs` cfvs) (tyCoVarsOfTypeDSet to_ty) to_ty
+        , AnnCast expr2 (c_ann, co) )
+      where
+        expr2 = go expr
+        cfvs  = tyCoVarsOfCoDSet co
+        c_ann = FVAnn cfvs (tyCoVarsOfTypeDSet co_ki) co_ki
+        co_ki = coercionType co
+        Just (_, to_ty) = splitCoercionType_maybe co_ki
+
+
+    go (Tick tickish expr)
+      = ( FVAnn { fva_fvs    = tickishFVs tickish `unionFVs` freeVarsOf expr2
+                , fva_ty_fvs = freeVarsOfType expr2
+                , fva_ty     = exprTypeFV expr2 }
+        , AnnTick tickish expr2 )
+      where
+        expr2 = go expr
+        tickishFVs (Breakpoint _ ids) = mkDVarSet ids
+        tickishFVs _                  = emptyDVarSet
+
+    go (Type ty) = ( FVAnn (tyCoVarsOfTypeDSet ty)
+                           (tyCoVarsOfTypeDSet ki)
+                           ki
+                   , AnnType ty)
+      where
+        ki = typeKind ty
 
-freeVars (Coercion co) = (runFVDSet $ tyCoVarsOfCoAcc co, AnnCoercion co)
+    go (Coercion co) = ( FVAnn (tyCoVarsOfCoDSet co)
+                               (tyCoVarsOfTypeDSet ki)
+                               ki
+                       , AnnCoercion co)
+      where
+        ki = coercionType co
index 10a93e5..0030e3c 100644 (file)
@@ -7,7 +7,6 @@ A ``lint'' pass to check for Core correctness
 -}
 
 {-# LANGUAGE CPP #-}
-{-# OPTIONS_GHC -fprof-auto #-}
 
 module CoreLint (
     lintCoreBindings, lintUnfolding,
@@ -31,7 +30,6 @@ import Bag
 import Literal
 import DataCon
 import TysWiredIn
-import TysPrim
 import TcType ( isFloatingTy )
 import Var
 import VarEnv
@@ -44,7 +42,7 @@ import Coercion
 import SrcLoc
 import Kind
 import Type
-import TypeRep
+import TyCoRep       -- checks validity of types/coercions
 import TyCon
 import CoAxiom
 import BasicTypes
@@ -78,12 +76,30 @@ This file implements the type-checking algorithm for System FC, the "official"
 name of the Core language. Type safety of FC is heart of the claim that
 executables produced by GHC do not have segmentation faults. Thus, it is
 useful to be able to reason about System FC independently of reading the code.
-To this purpose, there is a document ghc.pdf built in docs/core-spec that
+To this purpose, there is a document core-spec.pdf built in docs/core-spec that
 contains a formalism of the types and functions dealt with here. If you change
 just about anything in this file or you change other types/functions throughout
 the Core language (all signposted to this note), you should update that
 formalism. See docs/core-spec/README for more info about how to do so.
 
+Note [check vs lint]
+~~~~~~~~~~~~~~~~~~~~
+This file implements both a type checking algorithm and also general sanity
+checking. For example, the "sanity checking" checks for TyConApp on the left
+of an AppTy, which should never happen. These sanity checks don't really
+affect any notion of type soundness. Yet, it is convenient to do the sanity
+checks at the same time as the type checks. So, we use the following naming
+convention:
+
+- Functions that begin with 'lint'... are involved in type checking. These
+  functions might also do some sanity checking.
+
+- Functions that begin with 'check'... are *not* involved in type checking.
+  They exist only for sanity checking.
+
+Issues surrounding variable naming, shadowing, and such are considered *not*
+to be part of type checking, as the formalism omits these details.
+
 Summary of checks
 ~~~~~~~~~~~~~~~~~
 Checks that a set of core bindings is well-formed.  The PprStyle and String
@@ -120,14 +136,14 @@ That is, use a type let.   See Note [Type let] in CoreSyn.
 However, when linting <body> we need to remember that a=Int, else we might
 reject a correct program.  So we carry a type substitution (in this example
 [a -> Int]) and apply this substitution before comparing types.  The functin
-        lintInTy :: Type -> LintM Type
-returns a substituted type; that's the only reason it returns anything.
+        lintInTy :: Type -> LintM (Type, Kind)
+returns a substituted type.
 
 When we encounter a binder (like x::a) we must apply the substitution
 to the type of the binding variable.  lintBinders does this.
 
 For Ids, the type-substituted Id is added to the in_scope set (which
-itself is part of the TvSubst we are carrying down), and when we
+itself is part of the TCvSubst we are carrying down), and when we
 find an occurrence of an Id, we fetch it from the in-scope set.
 
 Note [Bad unsafe coercion]
@@ -337,7 +353,7 @@ interactiveInScope hsc_env
     te1    = mkTypeEnvWithImplicits (ic_tythings ictxt)
     te     = extendTypeEnvWithIds te1 (map instanceDFunId cls_insts)
     ids    = typeEnvIds te
-    tyvars = mapUnionVarSet (tyVarsOfType . idType) ids
+    tyvars = mapUnionVarSet (tyCoVarsOfType . idType) ids
               -- Why the type variables?  How can the top level envt have free tyvars?
               -- I think it's because of the GHCi debugger, which can bind variables
               --   f :: [t] -> [t]
@@ -453,7 +469,7 @@ lintSingleBinding top_lvl_flag rec_flag (binder,rhs)
     do { ty <- lintCoreExpr rhs
        ; lintBinder binder -- Check match to RHS type
        ; binder_ty <- applySubstTy (idType binder)
-       ; checkTys binder_ty ty (mkRhsMsg binder (ptext (sLit "RHS")) ty)
+       ; ensureEqTys binder_ty ty (mkRhsMsg binder (ptext (sLit "RHS")) ty)
 
         -- Check the let/app invariant
         -- See Note [CoreSyn let/app invariant] in CoreSyn
@@ -524,7 +540,7 @@ lintIdUnfolding :: Id -> Type -> Unfolding -> LintM ()
 lintIdUnfolding bndr bndr_ty (CoreUnfolding { uf_tmpl = rhs, uf_src = src })
   | isStableSource src
   = do { ty <- lintCoreExpr rhs
-       ; checkTys bndr_ty ty (mkRhsMsg bndr (ptext (sLit "unfolding")) ty) }
+       ; ensureEqTys bndr_ty ty (mkRhsMsg bndr (ptext (sLit "unfolding")) ty) }
 lintIdUnfolding  _ _ _
   = return ()       -- Do not Lint unstable unfoldings, because that leads
                     -- to exponential behaviour; c.f. CoreFVs.idUnfoldingVars
@@ -546,24 +562,23 @@ the desugarer.
 ************************************************************************
 -}
 
---type InKind      = Kind       -- Substitution not yet applied
 type InType      = Type
 type InCoercion  = Coercion
 type InVar       = Var
-type InTyVar     = TyVar
-
-type OutKind     = Kind -- Substitution has been applied to this,
-                        -- but has not been linted yet
-type LintedKind  = Kind -- Substitution applied, and type is linted
+type InTyVar     = Var
+type InCoVar     = Var
 
 type OutType     = Type -- Substitution has been applied to this,
                         -- but has not been linted yet
+type OutKind     = Kind
 
 type LintedType  = Type -- Substitution applied, and type is linted
+type LintedKind  = Kind
 
-type OutCoercion = Coercion
-type OutVar      = Var
-type OutTyVar    = TyVar
+type OutCoercion    = Coercion
+type OutVar         = Var
+type OutTyVar       = TyVar
+type OutCoVar       = Var
 
 lintCoreExpr :: CoreExpr -> LintM OutType
 -- The returned type has the substitution from the monad
@@ -591,9 +606,11 @@ lintCoreExpr (Lit lit)
 lintCoreExpr (Cast expr co)
   = do { expr_ty <- lintCoreExpr expr
        ; co' <- applySubstCo co
-       ; (_, from_ty, to_ty, r) <- lintCoercion co'
-       ; checkRole co' Representational r
-       ; checkTys from_ty expr_ty (mkCastErr expr co' from_ty expr_ty)
+       ; (_, k2, from_ty, to_ty, r) <- lintCoercion co'
+       ; lintL (classifiesTypeWithValues k2)
+               (ptext (sLit "Target of cast not # or *:") <+> ppr co)
+       ; lintRole co' Representational r
+       ; ensureEqTys from_ty expr_ty (mkCastErr expr co' from_ty expr_ty)
        ; return to_ty }
 
 lintCoreExpr (Tick (Breakpoint _ ids) expr)
@@ -610,7 +627,7 @@ lintCoreExpr (Let (NonRec tv (Type ty)) body)
   =     -- See Note [Linting type lets]
     do  { ty' <- applySubstTy ty
         ; lintTyBndr tv              $ \ tv' ->
-    do  { addLoc (RhsOf tv) $ checkTyKind tv' ty'
+    do  { addLoc (RhsOf tv) $ lintTyKind tv' ty'
                 -- Now extend the substitution so we
                 -- take advantage of it in the body
         ; extendSubstL tv' ty'       $
@@ -645,18 +662,13 @@ lintCoreExpr (Lam var expr)
   = addLoc (LambdaBodyOf var) $
     lintBinder var $ \ var' ->
     do { body_ty <- lintCoreExpr expr
-       ; if isId var' then
-             return (mkFunTy (idType var') body_ty)
-         else
-             return (mkForAllTy var' body_ty)
-       }
-        -- The applySubstTy is needed to apply the subst to var
+       ; return $ mkPiType var' body_ty }
 
 lintCoreExpr e@(Case scrut var alt_ty alts) =
        -- Check the scrutinee
   do { scrut_ty <- lintCoreExpr scrut
-     ; alt_ty   <- lintInTy alt_ty
-     ; var_ty   <- lintInTy (idType var)
+     ; (alt_ty, _) <- lintInTy alt_ty
+     ; (var_ty, _) <- lintInTy (idType var)
 
      -- See Note [No alternatives lint check]
      ; when (null alts) $
@@ -688,8 +700,8 @@ lintCoreExpr e@(Case scrut var alt_ty alts) =
 
         -- Don't use lintIdBndr on var, because unboxed tuple is legitimate
 
-     ; subst <- getTvSubst
-     ; checkTys var_ty scrut_ty (mkScrutMsg var var_ty scrut_ty subst)
+     ; subst <- getTCvSubst
+     ; ensureEqTys var_ty scrut_ty (mkScrutMsg var var_ty scrut_ty subst)
 
      ; lintAndScopeId var $ \_ ->
        do { -- Check the alternatives
@@ -703,29 +715,10 @@ lintCoreExpr (Type ty)
   = failWithL (ptext (sLit "Type found as expression") <+> ppr ty)
 
 lintCoreExpr (Coercion co)
-  = do { (_kind, ty1, ty2, role) <- lintInCo co
-       ; return (mkCoercionType role ty1 ty2) }
+  = do { (k1, k2, ty1, ty2, role) <- lintInCo co
+       ; return (mkHeteroCoercionType role k1 k2 ty1 ty2) }
 
 {-
-Note [Kind instantiation in coercions]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider the following coercion axiom:
-  ax_co [(k_ag :: BOX), (f_aa :: k_ag -> Constraint)] :: T k_ag f_aa ~ f_aa
-
-Consider the following instantiation:
-  ax_co <* -> *> <Monad>
-
-We need to split the co_ax_tvs into kind and type variables in order
-to find out the coercion kind instantiations. Those can only be Refl
-since we don't have kind coercions. This is just a way to represent
-kind instantiation.
-
-We use the number of kind variables to know how to split the coercions
-instantiations between kind coercions and type coercions. We lint the
-kind coercions and produce the following substitution which is to be
-applied in the type variables:
-  k_ag   ~~>   * -> *
-
 Note [No alternatives lint check]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Case expressions with no alternatives are odd beasts, and worth looking at
@@ -758,7 +751,10 @@ subtype of the required type, as one would expect.
 
 lintCoreArg  :: OutType -> CoreArg -> LintM OutType
 lintCoreArg fun_ty (Type arg_ty)
-  = do { arg_ty' <- applySubstTy arg_ty
+  = do { checkL (not (isCoercionTy arg_ty))
+                (ptext (sLit "Unnecessary coercion-to-type injection:")
+                  <+> ppr arg_ty)
+       ; arg_ty' <- applySubstTy arg_ty
        ; lintTyApp fun_ty arg_ty' }
 
 lintCoreArg fun_ty arg
@@ -775,7 +771,7 @@ lintAltBinders :: OutType     -- Scrutinee type
 -- If you edit this function, you may need to update the GHC formalism
 -- See Note [GHC Formalism]
 lintAltBinders scrut_ty con_ty []
-  = checkTys con_ty scrut_ty (mkBadPatMsg con_ty scrut_ty)
+  = ensureEqTys con_ty scrut_ty (mkBadPatMsg con_ty scrut_ty)
 lintAltBinders scrut_ty con_ty (bndr:bndrs)
   | isTyVar bndr
   = do { con_ty' <- lintTyApp con_ty (mkTyVarTy bndr)
@@ -787,10 +783,9 @@ lintAltBinders scrut_ty con_ty (bndr:bndrs)
 -----------------
 lintTyApp :: OutType -> OutType -> LintM OutType
 lintTyApp fun_ty arg_ty
-  | Just (tyvar,body_ty) <- splitForAllTy_maybe fun_ty
-  , isTyVar tyvar
-  = do  { checkTyKind tyvar arg_ty
-        ; return (substTyWith [tyvar] [arg_ty] body_ty) }
+  | Just (tv,body_ty) <- splitForAllTy_maybe fun_ty
+  = do  { lintTyKind tv arg_ty
+        ; return (substTyWith [tv] [arg_ty] body_ty) }
 
   | otherwise
   = failWithL (mkTyAppMsg fun_ty arg_ty)
@@ -799,7 +794,7 @@ lintTyApp fun_ty arg_ty
 lintValApp :: CoreExpr -> OutType -> OutType -> LintM OutType
 lintValApp arg fun_ty arg_ty
   | Just (arg,res) <- splitFunTy_maybe fun_ty
-  = do { checkTys arg arg_ty err1
+  = do { ensureEqTys arg arg_ty err1
        ; return res }
   | otherwise
   = failWithL err2
@@ -807,21 +802,18 @@ lintValApp arg fun_ty arg_ty
     err1 = mkAppMsg       fun_ty arg_ty arg
     err2 = mkNonFunAppMsg fun_ty arg_ty arg
 
-checkTyKind :: OutTyVar -> OutType -> LintM ()
+lintTyKind :: OutTyVar -> OutType -> LintM ()
 -- Both args have had substitution applied
 
 -- If you edit this function, you may need to update the GHC formalism
 -- See Note [GHC Formalism]
-checkTyKind tyvar arg_ty
-  | isSuperKind tyvar_kind  -- kind forall
-  = lintKind arg_ty
+lintTyKind tyvar arg_ty
         -- Arg type might be boxed for a function with an uncommitted
         -- tyvar; notably this is used so that we can give
         --      error :: forall a:*. String -> a
         -- and then apply it to both boxed and unboxed types.
-  | otherwise  -- type forall
   = do { arg_kind <- lintType arg_ty
-       ; unless (arg_kind `isSubKind` tyvar_kind)
+       ; unless (arg_kind `eqType` tyvar_kind)
                 (addErrL (mkKindErrMsg tyvar arg_ty $$ (text "xx" <+> ppr arg_kind))) }
   where
     tyvar_kind = tyVarKind tyvar
@@ -882,10 +874,10 @@ checkCaseAlts e ty alts =
                         Nothing    -> False
                         Just tycon -> isPrimTyCon tycon
 
-checkAltExpr :: CoreExpr -> OutType -> LintM ()
-checkAltExpr expr ann_ty
+lintAltExpr :: CoreExpr -> OutType -> LintM ()
+lintAltExpr expr ann_ty
   = do { actual_ty <- lintCoreExpr expr
-       ; checkTys actual_ty ann_ty (mkCaseAltMsg expr actual_ty ann_ty) }
+       ; ensureEqTys actual_ty ann_ty (mkCaseAltMsg expr actual_ty ann_ty) }
 
 lintCoreAlt :: OutType          -- Type of scrutinee
             -> OutType          -- Type of the alternative
@@ -894,16 +886,16 @@ lintCoreAlt :: OutType          -- Type of scrutinee
 -- If you edit this function, you may need to update the GHC formalism
 -- See Note [GHC Formalism]
 lintCoreAlt _ alt_ty (DEFAULT, args, rhs) =
-  do { checkL (null args) (mkDefaultArgsMsg args)
-     ; checkAltExpr rhs alt_ty }
+  do { lintL (null args) (mkDefaultArgsMsg args)
+     ; lintAltExpr rhs alt_ty }
 
 lintCoreAlt scrut_ty alt_ty (LitAlt lit, args, rhs)
   | litIsLifted lit
   = failWithL integerScrutinisedMsg
   | otherwise
-  = do { checkL (null args) (mkDefaultArgsMsg args)
-       ; checkTys lit_ty scrut_ty (mkBadPatMsg lit_ty scrut_ty)
-       ; checkAltExpr rhs alt_ty }
+  = do { lintL (null args) (mkDefaultArgsMsg args)
+       ; ensureEqTys lit_ty scrut_ty (mkBadPatMsg lit_ty scrut_ty)
+       ; lintAltExpr rhs alt_ty }
   where
     lit_ty = literalType lit
 
@@ -915,13 +907,13 @@ lintCoreAlt scrut_ty alt_ty alt@(DataAlt con, args, rhs)
     {   -- First instantiate the universally quantified
         -- type variables of the data constructor
         -- We've already check
-      checkL (tycon == dataConTyCon con) (mkBadConMsg tycon con)
+      lintL (tycon == dataConTyCon con) (mkBadConMsg tycon con)
     ; let con_payload_ty = applyTys (dataConRepType con) tycon_arg_tys
 
         -- And now bring the new binders into scope
     ; lintBinders args $ \ args' -> do
     { addLoc (CasePat alt) (lintAltBinders scrut_ty con_payload_ty args')
-    ; checkAltExpr rhs alt_ty } }
+    ; lintAltExpr rhs alt_ty } }
 
   | otherwise   -- Scrut-ty is wrong shape
   = addErrL (mkBadAltMsg scrut_ty alt)
@@ -948,15 +940,25 @@ lintBinders (var:vars) linterF = lintBinder var $ \var' ->
 -- See Note [GHC Formalism]
 lintBinder :: Var -> (Var -> LintM a) -> LintM a
 lintBinder var linterF
-  | isId var  = lintIdBndr var linterF
-  | otherwise = lintTyBndr var linterF
+  | isTyVar var = lintTyBndr var linterF
+  | isCoVar var = lintCoBndr var linterF
+  | otherwise   = lintIdBndr var linterF
 
 lintTyBndr :: InTyVar -> (OutTyVar -> LintM a) -> LintM a
 lintTyBndr tv thing_inside
-  = do { subst <- getTvSubst
-       ; let (subst', tv') = Type.substTyVarBndr subst tv
-       ; lintTyBndrKind tv'
-       ; updateTvSubst subst' (thing_inside tv') }
+  = do { subst <- getTCvSubst
+       ; let (subst', tv') = substTyVarBndr subst tv
+       ; lintKind (varType tv')
+       ; updateTCvSubst subst' (thing_inside tv') }
+
+lintCoBndr :: InCoVar -> (OutCoVar -> LintM a) -> LintM a
+lintCoBndr cv thing_inside
+  = do { subst <- getTCvSubst
+       ; let (subst', cv') = substCoVarBndr subst cv
+       ; lintKind (varType cv')
+       ; lintL (isCoercionType (varType cv'))
+               (text "CoVar with non-coercion type:" <+> pprTvBndr cv)
+       ; updateTCvSubst subst' (thing_inside cv') }
 
 lintIdBndr :: Id -> (Id -> LintM a) -> LintM a
 -- Do substitution on the type of a binder and add the var with this
@@ -981,36 +983,35 @@ lintAndScopeId id linterF
        ; checkL (not (lf_check_global_ids flags) || isLocalId id)
                 (ptext (sLit "Non-local Id binder") <+> ppr id)
                 -- See Note [Checking for global Ids]
-       ; ty <- lintInTy (idType id)
+       ; (ty, k) <- lintInTy (idType id)
+       ; lintL (not (isLevityPolymorphic k))
+           (text "Levity polymorphic binder:" <+>
+                 (ppr id <+> dcolon <+> parens (ppr ty <+> dcolon <+> ppr k)))
        ; let id' = setIdType id ty
        ; addInScopeVar id' $ (linterF id') }
 
 {-
-************************************************************************
-*                                                                      *
-             Types and kinds
-*                                                                      *
-************************************************************************
-
-We have a single linter for types and kinds.  That is convenient
-because sometimes it's not clear whether the thing we are looking
-at is a type or a kind.
+%************************************************************************
+%*                                                                      *
+             Types
+%*                                                                      *
+%************************************************************************
 -}
 
-lintInTy :: InType -> LintM LintedType
+lintInTy :: InType -> LintM (LintedType, LintedKind)
 -- Types only, not kinds
 -- Check the type, and apply the substitution to it
 -- See Note [Linting type lets]
 lintInTy ty
   = addLoc (InType ty) $
     do  { ty' <- applySubstTy ty
-        ; _k  <- lintType ty'
-        ; return ty' }
+        ; k  <- lintType ty'
+        ; lintKind k
+        ; return (ty', k) }
 
--------------------
-lintTyBndrKind :: OutTyVar -> LintM ()
--- Handles both type and kind foralls.
-lintTyBndrKind tv = lintKind (tyVarKind tv)
+checkTyCon :: TyCon -> LintM ()
+checkTyCon tc
+  = checkL (not (isTcTyCon tc)) (text "Found TcTyCon:" <+> ppr tc)
 
 -------------------
 lintType :: OutType -> LintM LintedKind
@@ -1019,57 +1020,83 @@ lintType :: OutType -> LintM LintedKind
 -- If you edit this function, you may need to update the GHC formalism
 -- See Note [GHC Formalism]
 lintType (TyVarTy tv)
-  = do { checkTyCoVarInScope tv
+  = do { checkL (isTyVar tv) (mkBadTyVarMsg tv)
+       ; lintTyCoVarInScope tv
        ; return (tyVarKind tv) }
          -- We checked its kind when we added it to the envt
 
 lintType ty@(AppTy t1 t2)
+  | TyConApp {} <- t1
+  = failWithL $ ptext (sLit "TyConApp to the left of AppTy:") <+> ppr ty
+  | otherwise
   = do { k1 <- lintType t1
        ; k2 <- lintType t2
        ; lint_ty_app ty k1 [(t2,k2)] }
 
-lintType ty@(FunTy t1 t2)    -- (->) has two different rules, for types and kinds
-  = do { k1 <- lintType t1
-       ; k2 <- lintType t2
-       ; lintArrow (ptext (sLit "type or kind") <+> quotes (ppr ty)) k1 k2 }
-
 lintType ty@(TyConApp tc tys)
   | Just ty' <- coreView ty
   = lintType ty'   -- Expand type synonyms, so that we do not bogusly complain
                    --  about un-saturated type synonyms
 
   | isUnLiftedTyCon tc || isTypeSynonymTyCon tc || isTypeFamilyTyCon tc
-       -- See Note [The kind invariant] in TypeRep
        -- Also type synonyms and type families
   , length tys < tyConArity tc
   = failWithL (hang (ptext (sLit "Un-saturated type application")) 2 (ppr ty))
 
   | otherwise
-  = do { ks <- mapM lintType tys
+  = do { checkTyCon tc
+       ; ks <- mapM lintType tys
        ; lint_ty_app ty (tyConKind tc) (tys `zip` ks) }
 
-lintType (ForAllTy tv ty)
-  = do { lintTyBndrKind tv
-       ; addInScopeVar tv (lintType ty) }
+-- arrows can related *unlifted* kinds, so this has to be separate from
+-- a dependent forall.
+lintType ty@(ForAllTy (Anon t1) t2)
+  = do { k1 <- lintType t1
+       ; k2 <- lintType t2
+       ; lintArrow (ptext (sLit "type or kind") <+> quotes (ppr ty)) k1 k2 }
+
+lintType t@(ForAllTy (Named tv _vis) ty)
+  = do { lintL (isTyVar tv) (text "Covar bound in type:" <+> ppr t)
+       ; lintTyBndr tv $ \tv' ->
+          do { k <- lintType ty
+             ; lintL (not (tv' `elemVarSet` tyCoVarsOfType k))
+                     (text "Variable escape in forall:" <+> ppr t)
+             ; lintL (classifiesTypeWithValues k)
+                     (text "Non-* and non-# kind in forall:" <+> ppr t)
+             ; return k }}
 
 lintType ty@(LitTy l) = lintTyLit l >> return (typeKind ty)
 
+lintType (CastTy ty co)
+  = do { k1 <- lintType ty
+       ; (k1', k2) <- lintStarCoercion co
+       ; ensureEqTys k1 k1' (mkCastErr ty co k1' k1)
+       ; return k2 }
+
+lintType (CoercionTy co)
+  = do { (k1, k2, ty1, ty2, r) <- lintCoercion co
+       ; return $ mkHeteroCoercionType r k1 k2 ty1 ty2 }
+
 lintKind :: OutKind -> LintM ()
 -- If you edit this function, you may need to update the GHC formalism
 -- See Note [GHC Formalism]
 lintKind k = do { sk <- lintType k
-                ; unless (isSuperKind sk)
+                ; unless ((isStarKind sk) || (isUnliftedTypeKind sk))
                          (addErrL (hang (ptext (sLit "Ill-kinded kind:") <+> ppr k)
                                       2 (ptext (sLit "has kind:") <+> ppr sk))) }
 
+-- confirms that a type is really *
+lintStar :: SDoc -> OutKind -> LintM ()
+lintStar doc k
+  = lintL (classifiesTypeWithValues k)
+          (ptext (sLit "Non-*-like kind when *-like expected:") <+> ppr k $$
+           ptext (sLit "when checking") <+> doc)
+
 lintArrow :: SDoc -> LintedKind -> LintedKind -> LintM LintedKind
 -- If you edit this function, you may need to update the GHC formalism
 -- See Note [GHC Formalism]
 lintArrow what k1 k2   -- Eg lintArrow "type or kind `blah'" k1 k2
                        -- or lintarrow "coercion `blah'" k1 k2
-  | isSuperKind k1
-  = return superKind
-  | otherwise
   = do { unless (okArrowArgKind k1)    (addErrL (msg (ptext (sLit "argument")) k1))
        ; unless (okArrowResultKind k2) (addErrL (msg (ptext (sLit "result"))   k2))
        ; return liftedTypeKind }
@@ -1115,13 +1142,13 @@ lint_app doc kfn kas
       | Just kfn' <- coreView kfn
       = go_app kfn' ka
 
-    go_app (FunTy kfa kfb) (_,ka)
-      = do { unless (ka `isSubKind` kfa) (addErrL fail_msg)
+    go_app (ForAllTy (Anon kfa) kfb) (_,ka)
+      = do { unless (ka `eqType` kfa) (addErrL fail_msg)
            ; return kfb }
 
-    go_app (ForAllTy kv kfn) (ta,ka)
-      = do { unless (ka `isSubKind` tyVarKind kv) (addErrL fail_msg)
-           ; return (substKiWith [kv] [ta] kfn) }
+    go_app (ForAllTy (Named kv _vis) kfn) (ta,ka)
+      = do { unless (ka `eqType` tyVarKind kv) (addErrL fail_msg)
+           ; return (substTyWith [kv] [ta] kfn) }
 
     go_app _ _ = failWithL fail_msg
 
@@ -1140,7 +1167,7 @@ lintCoreRule fun_ty (Rule { ru_name = name, ru_bndrs = bndrs
   = lintBinders bndrs $ \ _ ->
     do { lhs_ty <- foldM lintCoreArg fun_ty args
        ; rhs_ty <- lintCoreExpr rhs
-       ; checkTys lhs_ty rhs_ty $
+       ; ensureEqTys lhs_ty rhs_ty $
          (rule_doc <+> vcat [ ptext (sLit "lhs type:") <+> ppr lhs_ty
                             , ptext (sLit "rhs type:") <+> ppr rhs_ty ])
        ; let bad_bndrs = filterOut (`elemVarSet` exprsFreeVars args) bndrs
@@ -1176,7 +1203,7 @@ this check will nail it.
 ************************************************************************
 -}
 
-lintInCo :: InCoercion -> LintM (LintedKind, LintedType, LintedType, Role)
+lintInCo :: InCoercion -> LintM (LintedKind, LintedKind, LintedType, LintedType, Role)
 -- Check the coercion, and apply the substitution to it
 -- See Note [Linting type lets]
 lintInCo co
@@ -1184,79 +1211,109 @@ lintInCo co
     do  { co' <- applySubstCo co
         ; lintCoercion co' }
 
-lintCoercion :: OutCoercion -> LintM (LintedKind, LintedType, LintedType, Role)
+-- lints a coercion, confirming that its lh kind and its rh kind are both *
+-- also ensures that the role is Nominal
+lintStarCoercion :: OutCoercion -> LintM (LintedType, LintedType)
+lintStarCoercion g
+  = do { (k1, k2, t1, t2, r) <- lintCoercion g
+       ; lintStar (ptext (sLit "the kind of the left type in") <+> ppr g) k1
+       ; lintStar (ptext (sLit "the kind of the right type in") <+> ppr g) k2
+       ; lintRole g Nominal r
+       ; return (t1, t2) }
+
+lintCoercion :: OutCoercion -> LintM (LintedKind, LintedKind, LintedType, LintedType, Role)
 -- Check the kind of a coercion term, returning the kind
 -- Post-condition: the returned OutTypes are lint-free
---                 and have the same kind as each other
 
 -- If you edit this function, you may need to update the GHC formalism
 -- See Note [GHC Formalism]
 lintCoercion (Refl r ty)
   = do { k <- lintType ty
-       ; return (k, ty, ty, r) }
+       ; return (k, k, ty, ty, r) }
 
 lintCoercion co@(TyConAppCo r tc cos)
   | tc `hasKey` funTyConKey
   , [co1,co2] <- cos
-  = do { (k1,s1,t1,r1) <- lintCoercion co1
-       ; (k2,s2,t2,r2) <- lintCoercion co2
-       ; rk <- lintArrow (ptext (sLit "coercion") <+> quotes (ppr co)) k1 k2
-       ; checkRole co1 r r1
-       ; checkRole co2 r r2
-       ; return (rk, mkFunTy s1 s2, mkFunTy t1 t2, r) }
+  = do { (k1,k'1,s1,t1,r1) <- lintCoercion co1
+       ; (k2,k'2,s2,t2,r2) <- lintCoercion co2
+       ; k <- lintArrow (ptext (sLit "coercion") <+> quotes (ppr co)) k1 k2
+       ; k' <- lintArrow (ptext (sLit "coercion") <+> quotes (ppr co)) k'1 k'2
+       ; lintRole co1 r r1
+       ; lintRole co2 r r2
+       ; return (k, k', mkFunTy s1 s2, mkFunTy t1 t2, r) }
 
   | Just {} <- synTyConDefn_maybe tc
   = failWithL (ptext (sLit "Synonym in TyConAppCo:") <+> ppr co)
 
   | otherwise
-  = do { (ks,ss,ts,rs) <- mapAndUnzip4M lintCoercion cos
-       ; rk <- lint_co_app co (tyConKind tc) (ss `zip` ks)
-       ; _ <- zipWith3M checkRole cos (tyConRolesX r tc) rs
-       ; return (rk, mkTyConApp tc ss, mkTyConApp tc ts, r) }
+  = do { checkTyCon tc
+       ; (k's, ks, ss, ts, rs) <- mapAndUnzip5M lintCoercion cos
+       ; k' <- lint_co_app co (tyConKind tc) (ss `zip` k's)
+       ; k <- lint_co_app co (tyConKind tc) (ts `zip` ks)
+       ; _ <- zipWith3M lintRole cos (tyConRolesX r tc) rs
+       ; return (k', k, mkTyConApp tc ss, mkTyConApp tc ts, r) }
 
 lintCoercion co@(AppCo co1 co2)
-  = do { (k1,s1,t1,r1) <- lintCoercion co1
-       ; (k2,s2,t2,r2) <- lintCoercion co2
-       ; rk <- lint_co_app co k1 [(s2,k2)]
+  | TyConAppCo {} <- co1
+  = failWithL (ptext (sLit "TyConAppCo to the left of AppCo:") <+> ppr co)
+  | Refl _ (TyConApp {}) <- co1
+  = failWithL (ptext (sLit "Refl (TyConApp ...) to the left of AppCo:") <+> ppr co)
+  | otherwise
+  = do { (k1,k2,s1,s2,r1) <- lintCoercion co1
+       ; (k'1, k'2, t1, t2, r2) <- lintCoercion co2
+       ; k3 <- lint_co_app co k1 [(t1,k'1)]
+       ; k4 <- lint_co_app co k2 [(t2,k'2)]
        ; if r1 == Phantom
-         then checkL (r2 == Phantom || r2 == Nominal)
+         then lintL (r2 == Phantom || r2 == Nominal)
                      (ptext (sLit "Second argument in AppCo cannot be R:") $$
                       ppr co)
-         else checkRole co Nominal r2
-       ; return (rk, mkAppTy s1 s2, mkAppTy t1 t2, r1) }
-
-lintCoercion (ForAllCo tv co)
-  = do { lintTyBndrKind tv
-       ; (k, s, t, r) <- addInScopeVar tv (lintCoercion co)
-       ; return (k, mkForAllTy tv s, mkForAllTy tv t, r) }
+         else lintRole co Nominal r2
+       ; return (k3, k4, mkAppTy s1 t1, mkAppTy s2 t2, r1) }
+
+----------
+lintCoercion (ForAllCo tv1 kind_co co)
+  = do { (_, k2) <- lintStarCoercion kind_co
+       ; let tv2 = setTyVarKind tv1 k2
+       ; (k3, k4, t1, t2, r) <- addInScopeVar tv1 $ lintCoercion co
+       ; let tyl = mkNamedForAllTy tv1 Invisible t1
+             tyr = mkNamedForAllTy tv2 Invisible $
+                   substTyWith [tv1] [TyVarTy tv2 `mkCastTy` mkSymCo kind_co] t2
+       ; return (k3, k4, tyl, tyr, r) }
 
 lintCoercion (CoVarCo cv)
   | not (isCoVar cv)
   = failWithL (hang (ptext (sLit "Bad CoVarCo:") <+> ppr cv)
                   2 (ptext (sLit "With offending type:") <+> ppr (varType cv)))
   | otherwise
-  = do { checkTyCoVarInScope cv
+  = do { lintTyCoVarInScope cv
        ; cv' <- lookupIdInScope cv
-       ; let (s,t) = coVarKind cv'
-             k     = typeKind s
-             r     = coVarRole cv'
-       ; when (isSuperKind k) $
-         do { checkL (r == Nominal) (hang (ptext (sLit "Non-nominal kind equality"))
-                                     2 (ppr cv))
-            ; checkL (s `eqKind` t) (hang (ptext (sLit "Non-refl kind equality"))
-                                     2 (ppr cv)) }
-       ; return (k, s, t, r) }
+       ; lintUnLiftedCoVar cv
+       ; return $ coVarKindsTypesRole cv' }
 
 -- See Note [Bad unsafe coercion]
-lintCoercion (UnivCo _prov r ty1 ty2)
+lintCoercion co@(UnivCo prov r ty1 ty2)
   = do { k1 <- lintType ty1
        ; k2 <- lintType ty2
---       ; unless (k1 `eqKind` k2) $
---         failWithL (hang (ptext (sLit "Unsafe coercion changes kind"))
---                       2 (ppr co))
-       ; when (r /= Phantom && isSubOpenTypeKind k1 && isSubOpenTypeKind k2)
+       ; case prov of
+           UnsafeCoerceProv -> return ()  -- no extra checks
+
+           PhantomProv kco    -> do { lintRole co Phantom r
+                                    ; check_kinds kco k1 k2 }
+
+           ProofIrrelProv kco -> do { lintL (isCoercionTy ty1) $
+                                          mkBadProofIrrelMsg ty1 co
+                                    ; lintL (isCoercionTy ty2) $
+                                          mkBadProofIrrelMsg ty2 co
+                                    ; check_kinds kco k1 k2 }
+
+           PluginProv _     -> return ()  -- no extra checks
+           HoleProv h       -> addErrL $
+                               text "Unfilled coercion hole:" <+> ppr h
+
+       ; when (r /= Phantom && classifiesTypeWithValues k1
+                            && classifiesTypeWithValues k2)
               (checkTypes ty1 ty2)
-       ; return (k1, ty1, ty2, r) }
+       ; return (k1, k2, ty1, ty2, r) }
    where
      report s = hang (text $ "Unsafe coercion between " ++ s)
                      2 (vcat [ text "From:" <+> ppr ty1
@@ -1290,60 +1347,80 @@ lintCoercion (UnivCo _prov r ty1 ty2)
                 _          -> return ()
             }
 
+     check_kinds kco k1 k2 = do { (k1', k2') <- lintStarCoercion kco
+                                ; ensureEqTys k1 k1' (mkBadUnivCoMsg CLeft  co)
+                                ; ensureEqTys k2 k2' (mkBadUnivCoMsg CRight co) }
+
+
 lintCoercion (SymCo co)
-  = do { (k, ty1, ty2, r) <- lintCoercion co
-       ; return (k, ty2, ty1, r) }
+  = do { (k1, k2, ty1, ty2, r) <- lintCoercion co
+       ; return (k2, k1, ty2, ty1, r) }
 
 lintCoercion co@(TransCo co1 co2)
-  = do { (k1, ty1a, ty1b, r1) <- lintCoercion co1
-       ; (_ ty2a, ty2b, r2) <- lintCoercion co2
-       ; checkL (ty1b `eqType` ty2a)
-                (hang (ptext (sLit "Trans coercion mis-match:") <+> ppr co)
-                    2 (vcat [ppr ty1a, ppr ty1b, ppr ty2a, ppr ty2b]))
-       ; checkRole co r1 r2
-       ; return (k1, ty1a, ty2b, r1) }
+  = do { (k1a, _k1b, ty1a, ty1b, r1) <- lintCoercion co1
+       ; (_k2a, k2b, ty2a, ty2b, r2) <- lintCoercion co2
+       ; ensureEqTys ty1b ty2a
+               (hang (ptext (sLit "Trans coercion mis-match:") <+> ppr co)
+                   2 (vcat [ppr ty1a, ppr ty1b, ppr ty2a, ppr ty2b]))
+       ; lintRole co r1 r2
+       ; return (k1a, k2b, ty1a, ty2b, r1) }
 
 lintCoercion the_co@(NthCo n co)
-  = do { (_,s,t,r) <- lintCoercion co
-       ; case (splitTyConApp_maybe s, splitTyConApp_maybe t) of
-           (Just (tc_s, tys_s), Just (tc_t, tys_t))
+  = do { (_, _, s, t, r) <- lintCoercion co
+       ; case (splitForAllTy_maybe s, splitForAllTy_maybe t) of
+         { (Just (tv_s, _ty_s), Just (tv_t, _ty_t))
+             |  n == 0
+             -> return (ks, kt, ts, tt, Nominal)
+             where
+               ts = tyVarKind tv_s
+               tt = tyVarKind tv_t
+               ks = typeKind ts
+               kt = typeKind tt
+
+         ; _ -> case (splitTyConApp_maybe s, splitTyConApp_maybe t) of
+         { (Just (tc_s, tys_s), Just (tc_t, tys_t))
              | tc_s == tc_t
              , isInjectiveTyCon tc_s r
-                 -- see Note [NthCo and newtypes] in Coercion
+                 -- see Note [NthCo and newtypes] in TyCoRep
              , tys_s `equalLength` tys_t
              , n < length tys_s
-             -> return (ks, ts, tt, tr)
+             -> return (ks, kt, ts, tt, tr)
              where
                ts = getNth tys_s n
                tt = getNth tys_t n
                tr = nthRole r tc_s n
                ks = typeKind ts
+               kt = typeKind tt
 
-           _ -> failWithL (hang (ptext (sLit "Bad getNth:"))
-                              2 (ppr the_co $$ ppr s $$ ppr t)) }
+         ; _ -> failWithL (hang (ptext (sLit "Bad getNth:"))
+                              2 (ppr the_co $$ ppr s $$ ppr t)) }}}
 
 lintCoercion the_co@(LRCo lr co)
-  = do { (_,s,t,r) <- lintCoercion co
-       ; checkRole co Nominal r
+  = do { (_,_,s,t,r) <- lintCoercion co
+       ; lintRole co Nominal r
        ; case (splitAppTy_maybe s, splitAppTy_maybe t) of
            (Just s_pr, Just t_pr)
-             -> return (k, s_pick, t_pick, Nominal)
+             -> return (ks_pick, kt_pick, s_pick, t_pick, Nominal)
              where
-               s_pick = pickLR lr s_pr
-               t_pick = pickLR lr t_pr
-               k = typeKind s_pick
+               s_pick  = pickLR lr s_pr
+               t_pick  = pickLR lr t_pr
+               ks_pick = typeKind s_pick
+               kt_pick = typeKind t_pick
 
            _ -> failWithL (hang (ptext (sLit "Bad LRCo:"))
                               2 (ppr the_co $$ ppr s $$ ppr t)) }
 
-lintCoercion (InstCo co arg_ty)
-  = do { (k,s,t,r) <- lintCoercion co
-       ; arg_kind  <- lintType arg_ty
-       ; case (splitForAllTy_maybe s, splitForAllTy_maybe t) of
-          (Just (tv1,ty1), Just (tv2,ty2))
-            | arg_kind `isSubKind` tyVarKind tv1
-            -> return (k, substTyWith [tv1] [arg_ty] ty1,
-                          substTyWith [tv2] [arg_ty] ty2, r)
+lintCoercion (InstCo co arg)
+  = do { (k3, k4, t1',t2', r) <- lintCoercion co
+       ; (k1',k2',s1,s2, r') <- lintCoercion arg
+       ; lintRole arg Nominal r'
+       ; case (splitForAllTy_maybe t1', splitForAllTy_maybe t2') of
+          (Just (tv1,t1), Just (tv2,t2))
+            | k1' `eqType` tyVarKind tv1
+            , k2' `eqType` tyVarKind tv2
+            -> return (k3, k4,
+                       substTyWith [tv1] [s1] t1,
+                       substTyWith [tv2] [s2] t2, r)
             | otherwise
             -> failWithL (ptext (sLit "Kind mis-match in inst coercion"))
           _ -> failWithL (ptext (sLit "Bad argument of inst")) }
@@ -1351,90 +1428,89 @@ lintCoercion (InstCo co arg_ty)
 lintCoercion co@(AxiomInstCo con ind cos)
   = do { unless (0 <= ind && ind < numBranches (coAxiomBranches con))
                 (bad_ax (text "index out of range"))
-         -- See Note [Kind instantiation in coercions]
        ; let CoAxBranch { cab_tvs   = ktvs
+                        , cab_cvs   = cvs
                         , cab_roles = roles
                         , cab_lhs   = lhs
                         , cab_rhs   = rhs } = coAxiomNthBranch con ind
-       ; unless (equalLength ktvs cos) (bad_ax (text "lengths"))
-       ; in_scope <- getInScope
-       ; let empty_subst = mkTvSubst in_scope emptyTvSubstEnv
+       ; unless (length ktvs + length cvs == length cos) $
+           bad_ax (text "lengths")
+       ; subst <- getTCvSubst
+       ; let empty_subst = zapTCvSubst subst
        ; (subst_l, subst_r) <- foldlM check_ki
                                       (empty_subst, empty_subst)
-                                      (zip3 ktvs roles cos)
-       ; let lhs' = Type.substTys subst_l lhs
-             rhs' = Type.substTy subst_r rhs
+                                      (zip3 (ktvs ++ cvs) roles cos)
+       ; let lhs' = substTys subst_l lhs
+             rhs' = substTy subst_r rhs
        ; case checkAxInstCo co of
            Just bad_branch -> bad_ax $ text "inconsistent with" <+>
                                        pprCoAxBranch con bad_branch
            Nothing -> return ()
-       ; return (typeKind rhs', mkTyConApp (coAxiomTyCon con) lhs', rhs', coAxiomRole con) }
+       ; let s2 = mkTyConApp (coAxiomTyCon con) lhs'
+       ; return (typeKind s2, typeKind rhs', s2, rhs', coAxiomRole con) }
   where
     bad_ax what = addErrL (hang (text  "Bad axiom application" <+> parens what)
                         2 (ppr co))
 
-    check_ki (subst_l, subst_r) (ktv, role, co)
-      = do { (k, t1, t2, r) <- lintCoercion co
-           ; checkRole co role r
-           ; let ktv_kind = Type.substTy subst_l (tyVarKind ktv)
-                  -- Using subst_l is ok, because subst_l and subst_r
-                  -- must agree on kind equalities
-           ; unless (k `isSubKind` ktv_kind)
-                    (bad_ax (text "check_ki2" <+>
-                             vcat [ ppr co, ppr k, ppr ktv, ppr ktv_kind ] ))
-           ; return (Type.extendTvSubst subst_l ktv t1,
-                     Type.extendTvSubst subst_r ktv t2) }
-
-lintCoercion co@(SubCo co')
-  = do { (k,s,t,r) <- lintCoercion co'
-       ; checkRole co Nominal r
-       ; return (k,s,t,Representational) }
-
-
-lintCoercion this@(AxiomRuleCo co ts cs)
-  = do _ks <- mapM lintType ts
-       eqs <- mapM lintCoercion cs
-
-       let tyNum = length ts
-
-       case compare (coaxrTypeArity co) tyNum of
-         EQ -> return ()
-         LT -> err "Too many type arguments"
-                    [ txt "expected" <+> int (coaxrTypeArity co)
-                    , txt "provided" <+> int tyNum ]
-         GT -> err "Not enough type arguments"
-                    [ txt "expected" <+> int (coaxrTypeArity co)
-                          , txt "provided" <+> int tyNum ]
-       checkRoles 0 (coaxrAsmpRoles co) eqs
-
-       case coaxrProves co ts [ Pair l r | (_,l,r,_) <- eqs ] of
-         Nothing -> err "Malformed use of AxiomRuleCo" [ ppr this ]
-         Just (Pair l r) ->
-           do kL <- lintType l
-              kR <- lintType r
-              unless (eqKind kL kR)
-                $ err "Kind error in CoAxiomRule"
-                       [ppr kL <+> txt "/=" <+> ppr kR]
-              return (kL, l, r, coaxrRole co)
+    check_ki (subst_l, subst_r) (ktv, role, arg)
+      = do { (k', k'', s', t', r) <- lintCoercion arg
+           ; lintRole arg role r
+           ; let ktv_kind_l = substTy subst_l (tyVarKind ktv)
+                 ktv_kind_r = substTy subst_r (tyVarKind ktv)
+           ; unless (k' `eqType` ktv_kind_l)
+                    (bad_ax (text "check_ki1" <+> vcat [ ppr co, ppr k', ppr ktv, ppr ktv_kind_l ] ))
+           ; unless (k'' `eqType` ktv_kind_r)
+                    (bad_ax (text "check_ki2" <+> vcat [ ppr co, ppr k'', ppr ktv, ppr ktv_kind_r ] ))
+           ; return (extendTCvSubst subst_l ktv s',
+                     extendTCvSubst subst_r ktv t') }
+
+lintCoercion (CoherenceCo co1 co2)
+  = do { (_, k2, t1, t2, r) <- lintCoercion co1
+       ; let lhsty = mkCastTy t1 co2
+       ; k1' <- lintType lhsty
+       ; return (k1', k2, lhsty, t2, r) }
+
+lintCoercion (KindCo co)
+  = do { (k1, k2, _, _, _) <- lintCoercion co
+       ; return (liftedTypeKind, liftedTypeKind, k1, k2, Nominal) }
+
+lintCoercion (SubCo co')
+  = do { (k1,k2,s,t,r) <- lintCoercion co'
+       ; lintRole co' Nominal r
+       ; return (k1,k2,s,t,Representational) }
+
+lintCoercion this@(AxiomRuleCo co cs)
+  = do { eqs <- mapM lintCoercion cs
+       ; lintRoles 0 (coaxrAsmpRoles co) eqs
+       ; case coaxrProves co [ Pair l r | (_,_,l,r,_) <- eqs ] of
+           Nothing -> err "Malformed use of AxiomRuleCo" [ ppr this ]
+           Just (Pair l r) ->
+             return (typeKind l, typeKind r, l, r, coaxrRole co) }
   where
-  txt       = ptext . sLit
   err m xs  = failWithL $
-                hang (txt m) 2 $ vcat (txt "Rule:" <+> ppr (coaxrName co) : xs)
+                hang (text m) 2 $ vcat (text "Rule:" <+> ppr (coaxrName co) : xs)
 
-  checkRoles n (e : es) ((_,_,_,r) : rs)
-    | e == r    = checkRoles (n+1) es rs
+  lintRoles n (e : es) ((_,_,_,_,r) : rs)
+    | e == r    = lintRoles (n+1) es rs
     | otherwise = err "Argument roles mismatch"
-                      [ txt "In argument:" <+> int (n+1)
-                      , txt "Expected:" <+> ppr e
-                      , txt "Found:" <+> ppr r ]
-  checkRoles _ [] []  = return ()
-  checkRoles n [] rs  = err "Too many coercion arguments"
-                          [ txt "Expected:" <+> int n
-                          , txt "Provided:" <+> int (n + length rs) ]
-
-  checkRoles n es []  = err "Not enough coercion arguments"
-                          [ txt "Expected:" <+> int (n + length es)
-                          , txt "Provided:" <+> int n ]
+                      [ text "In argument:" <+> int (n+1)
+                      , text "Expected:" <+> ppr e
+                      , text "Found:" <+> ppr r ]
+  lintRoles _ [] []  = return ()
+  lintRoles n [] rs  = err "Too many coercion arguments"
+                          [ text "Expected:" <+> int n
+                          , text "Provided:" <+> int (n + length rs) ]
+
+  lintRoles n es []  = err "Not enough coercion arguments"
+                          [ text "Expected:" <+> int (n + length es)
+                          , text "Provided:" <+> int n ]
+
+----------
+lintUnLiftedCoVar :: CoVar -> LintM ()
+lintUnLiftedCoVar cv
+  = when (not (isUnLiftedType (coVarKind cv))) $
+    failWithL (text "Bad lifted equality:" <+> ppr cv
+                 <+> dcolon <+> ppr (coVarKind cv))
 
 {-
 ************************************************************************
@@ -1449,7 +1525,7 @@ lintCoercion this@(AxiomRuleCo co ts cs)
 data LintEnv
   = LE { le_flags :: LintFlags       -- Linting the result of this pass
        , le_loc   :: [LintLocInfo]   -- Locations
-       , le_subst :: TvSubst         -- Current type substitution; we also use this
+       , le_subst :: TCvSubst        -- Current type substitution; we also use this
                                      -- to keep track of all the variables in scope,
                                      -- both Ids and TyVars
        , le_dynflags :: DynFlags     -- DynamicFlags
@@ -1533,7 +1609,7 @@ initL dflags flags m
   = case unLintM m env (emptyBag, emptyBag) of
       (_, errs) -> errs
   where
-    env = LE { le_flags = flags, le_subst = emptyTvSubst, le_loc = [], le_dynflags = dflags }
+    env = LE { le_flags = flags, le_subst = emptyTCvSubst, le_loc = [], le_dynflags = dflags }
 
 getLintFlags :: LintM LintFlags
 getLintFlags = LintM $ \ env errs -> (Just (le_flags env), errs)
@@ -1542,6 +1618,10 @@ checkL :: Bool -> MsgDoc -> LintM ()
 checkL True  _   = return ()
 checkL False msg = failWithL msg
 
+-- like checkL, but relevant to type checking
+lintL :: Bool -> MsgDoc -> LintM ()
+lintL = checkL
+
 checkWarnL :: Bool -> MsgDoc -> LintM ()
 checkWarnL True   _  = return ()
 checkWarnL False msg = addWarnL msg
@@ -1586,42 +1666,39 @@ inCasePat = LintM $ \ env errs -> (Just (is_case_pat env), errs)
 addInScopeVars :: [Var] -> LintM a -> LintM a
 addInScopeVars vars m
   = LintM $ \ env errs ->
-    unLintM m (env { le_subst = extendTvInScopeList (le_subst env) vars })
+    unLintM m (env { le_subst = extendTCvInScopeList (le_subst env) vars })
               errs
 
 addInScopeVar :: Var -> LintM a -> LintM a
 addInScopeVar var m
   = LintM $ \ env errs ->
-    unLintM m (env { le_subst = extendTvInScope (le_subst env) var }) errs
+    unLintM m (env { le_subst = extendTCvInScope (le_subst env) var }) errs
 
 extendSubstL :: TyVar -> Type -> LintM a -> LintM a
 extendSubstL tv ty m
   = LintM $ \ env errs ->
-    unLintM m (env { le_subst = Type.extendTvSubst (le_subst env) tv ty }) errs
+    unLintM m (env { le_subst = Type.extendTCvSubst (le_subst env) tv ty }) errs
 
-updateTvSubst :: TvSubst -> LintM a -> LintM a
-updateTvSubst subst' m
+updateTCvSubst :: TCvSubst -> LintM a -> LintM a
+updateTCvSubst subst' m
   = LintM $ \ env errs -> unLintM m (env { le_subst = subst' }) errs
 
-getTvSubst :: LintM TvSubst
-getTvSubst = LintM (\ env errs -> (Just (le_subst env), errs))
-
-getInScope :: LintM InScopeSet
-getInScope = LintM (\ env errs -> (Just (getTvInScope (le_subst env)), errs))
+getTCvSubst :: LintM TCvSubst
+getTCvSubst = LintM (\ env errs -> (Just (le_subst env), errs))
 
 applySubstTy :: InType -> LintM OutType
-applySubstTy ty = do { subst <- getTvSubst; return (Type.substTy subst ty) }
+applySubstTy ty = do { subst <- getTCvSubst; return (substTy subst ty) }
 
 applySubstCo :: InCoercion -> LintM OutCoercion
-applySubstCo co = do { subst <- getTvSubst; return (substCo (tvCvSubst subst) co) }
+applySubstCo co = do { subst <- getTCvSubst; return (substCo subst co) }
 
 lookupIdInScope :: Id -> LintM Id
 lookupIdInScope id
   | not (mustHaveLocalBinding id)
   = return id   -- An imported Id
   | otherwise
-  = do  { subst <- getTvSubst
-        ; case lookupInScope (getTvInScope subst) id of
+  = do  { subst <- getTCvSubst
+        ; case lookupInScope (getTCvInScope subst) id of
                 Just v  -> return v
                 Nothing -> do { addErrL out_of_scope
                               ; return id } }
@@ -1632,30 +1709,31 @@ lookupIdInScope id
 oneTupleDataConId :: Id -- Should not happen
 oneTupleDataConId = dataConWorkId (tupleDataCon Boxed 1)
 
-checkTyCoVarInScope :: Var -> LintM ()
-checkTyCoVarInScope v = checkInScope (ptext (sLit "is out of scope")) v
+lintTyCoVarInScope :: Var -> LintM ()
+lintTyCoVarInScope v = lintInScope (ptext (sLit "is out of scope")) v
 
-checkInScope :: SDoc -> Var -> LintM ()
-checkInScope loc_msg var =
- do { subst <- getTvSubst
-    ; checkL (not (mustHaveLocalBinding var) || (var `isInScope` subst))
+lintInScope :: SDoc -> Var -> LintM ()
+lintInScope loc_msg var =
+ do { subst <- getTCvSubst
+    ; lintL (not (mustHaveLocalBinding var) || (var `isInScope` subst))
              (hsep [pprBndr LetBind var, loc_msg]) }
 
-checkTys :: OutType -> OutType -> MsgDoc -> LintM ()
+ensureEqTys :: OutType -> OutType -> MsgDoc -> LintM ()
 -- check ty2 is subtype of ty1 (ie, has same structure but usage
 -- annotations need only be consistent, not equal)
 -- Assumes ty1,ty2 are have alrady had the substitution applied
-checkTys ty1 ty2 msg = checkL (ty1 `eqType` ty2) msg
+ensureEqTys ty1 ty2 msg = lintL (ty1 `eqType` ty2) msg
 
-checkRole :: Coercion
+lintRole :: Outputable thing
+          => thing     -- where the role appeared
           -> Role      -- expected
           -> Role      -- actual
           -> LintM ()
-checkRole co r1 r2
-  = checkL (r1 == r2)
-           (ptext (sLit "Role incompatibility: expected") <+> ppr r1 <> comma <+>
-            ptext (sLit "got") <+> ppr r2 $$
-            ptext (sLit "in") <+> ppr co)
+lintRole co r1 r2
+  = lintL (r1 == r2)
+          (ptext (sLit "Role incompatibility: expected") <+> ppr r1 <> comma <+>
+           ptext (sLit "got") <+> ppr r2 $$
+           ptext (sLit "in") <+> ppr co)
 
 {-
 ************************************************************************
@@ -1717,12 +1795,12 @@ mkCaseAltMsg e ty1 ty2
   = hang (text "Type of case alternatives not the same as the annotation on case:")
          4 (vcat [ppr ty1, ppr ty2, ppr e])
 
-mkScrutMsg :: Id -> Type -> Type -> TvSubst -> MsgDoc
+mkScrutMsg :: Id -> Type -> Type -> TCvSubst -> MsgDoc
 mkScrutMsg var var_ty scrut_ty subst
   = vcat [text "Result binder in case doesn't match scrutinee:" <+> ppr var,
           text "Result binder type:" <+> ppr var_ty,--(idType var),
           text "Scrutinee type:" <+> ppr scrut_ty,
-     hsep [ptext (sLit "Current TV subst"), ppr subst]]
+     hsep [ptext (sLit "Current TCv subst"), ppr subst]]
 
 mkNonDefltMsg, mkNonIncreasingAltsMsg :: CoreExpr -> MsgDoc
 mkNonDefltMsg e
@@ -1857,7 +1935,7 @@ mkArityMsg binder
          ]
            where (StrictSig dmd_ty) = idStrictness binder
 -}
-mkCastErr :: CoreExpr -> Coercion -> Type -> Type -> MsgDoc
+mkCastErr :: Outputable casted => casted -> Coercion -> Type -> Type -> MsgDoc
 mkCastErr expr co from_ty expr_ty
   = vcat [ptext (sLit "From-type of Cast differs from type of enclosed expression"),
           ptext (sLit "From-type:") <+> ppr from_ty,
@@ -1866,6 +1944,26 @@ mkCastErr expr co from_ty expr_ty
           ptext (sLit "Coercion used in cast:") <+> ppr co
          ]
 
+mkBadUnivCoMsg :: LeftOrRight -> Coercion -> SDoc
+mkBadUnivCoMsg lr co
+  = text "Kind mismatch on the" <+> pprLeftOrRight lr <+>
+    text "side of a UnivCo:" <+> ppr co
+
+mkBadProofIrrelMsg :: Type -> Coercion -> SDoc
+mkBadProofIrrelMsg ty co
+  = hang (text "Found a non-coercion in a proof-irrelevance UnivCo:")
+       2 (vcat [ text "type:" <+> ppr ty
+               , text "co:" <+> ppr co ])
+
+mkBadTyVarMsg :: Var -> SDoc
+mkBadTyVarMsg tv
+  = ptext (sLit "Non-tyvar used in TyVarTy:")
+      <+> ppr tv <+> dcolon <+> ppr (varType tv)
+
+pprLeftOrRight :: LeftOrRight -> MsgDoc
+pprLeftOrRight CLeft  = ptext (sLit "left")
+pprLeftOrRight CRight = ptext (sLit "right")
+
 dupVars :: [[Var]] -> MsgDoc
 dupVars vars
   = hang (ptext (sLit "Duplicate variables brought into scope"))
index 999ca54..70eb1a1 100644 (file)
@@ -516,6 +516,7 @@ cpeRhsE env (Var f `App` _{-type-} `App` arg)
   | f `hasKey` lazyIdKey          -- Replace (lazy a) by a
   = cpeRhsE env arg               -- See Note [lazyId magic] in MkId
 
+cpeRhsE env (Var f `App` _{-levity-} `App` _{-type-} `App` arg)
     -- See Note [runRW magic] in MkId
   | f `hasKey` runRWKey           -- Replace (runRW# f) by (f realWorld#),
   = case arg of                   -- beta reducing if possible
@@ -680,11 +681,11 @@ cpeApp env expr
 
     collect_args (App fun arg@(Type arg_ty)) depth
       = do { (fun',hd,fun_ty,floats,ss) <- collect_args fun depth
-           ; return (App fun' arg, hd, applyTy fun_ty arg_ty, floats, ss) }
+           ; return (App fun' arg, hd, piResultTy fun_ty arg_ty, floats, ss) }
 
-    collect_args (App fun arg@(Coercion arg_co)) depth
+    collect_args (App fun arg@(Coercion {})) depth
       = do { (fun',hd,fun_ty,floats,ss) <- collect_args fun depth
-           ; return (App fun' arg, hd, applyCo fun_ty arg_co, floats, ss) }
+           ; return (App fun' arg, hd, funResultTy fun_ty, floats, ss) }
 
     collect_args (App fun arg) depth
       = do { (fun',hd,fun_ty,floats,ss) <- collect_args fun (depth+1)
@@ -1127,7 +1128,7 @@ canFloatFromNoCaf platform (Floats ok_to_spec fs) rhs
     -- any non-static things or it would *already* be Caffy
     rhs_ok = rhsIsStatic platform (\_ -> False)
                          (\i -> pprPanic "rhsIsStatic" (integer i))
-                         -- Integer literals should not show up 
+                         -- Integer literals should not show up
 
 wantFloatNested :: RecFlag -> Bool -> Floats -> CpeRhs -> Bool
 wantFloatNested is_rec strict_or_unlifted floats rhs
@@ -1258,7 +1259,7 @@ newVar :: Type -> UniqSM Id
 newVar ty
  = seqType ty `seq` do
      uniq <- getUniqueM
-     return (mkSysLocal (fsLit "sat") uniq ty)
+     return (mkSysLocalOrCoVar (fsLit "sat") uniq ty)
 
 
 ------------------------------------------------------------------------------
index 697ce4b..0668816 100644 (file)
@@ -16,13 +16,12 @@ module CoreSubst (
         deShadowBinds, substSpec, substRulesForImportedIds,
         substTy, substCo, substExpr, substExprSC, substBind, substBindSC,
         substUnfolding, substUnfoldingSC,
-        lookupIdSubst, lookupTvSubst, lookupCvSubst, substIdOcc,
+        lookupIdSubst, lookupTCvSubst, substIdOcc,
         substTickish, substDVarSet,
 
         -- ** Operations on substitutions
         emptySubst, mkEmptySubst, mkSubst, mkOpenSubst, substInScope, isEmptySubst,
-        extendIdSubst, extendIdSubstList, extendTvSubst, extendTvSubstList,
-        extendCvSubst, extendCvSubstList,
+        extendIdSubst, extendIdSubstList, extendTCvSubst, extendTCvSubstList,
         extendSubst, extendSubstList, extendSubstWithVar, zapSubstEnv,
         addInScopeSet, extendInScope, extendInScopeList, extendInScopeIds,
         isInScope, setInScope,
@@ -51,14 +50,13 @@ import qualified Type
 import qualified Coercion
 
         -- We are defining local versions
-import Type     hiding ( substTy, extendTvSubst, extendTvSubstList
+import Type     hiding ( substTy, extendTCvSubst, extendTCvSubstList
                        , isInScope, substTyVarBndr, cloneTyVarBndr )
-import TypeRep (tyVarsOfTypeAcc)
-import Coercion hiding ( substTy, substCo, extendTvSubst, substTyVarBndr, substCoVarBndr )
+import Coercion hiding ( substCo, substCoVarBndr )
 
 import TyCon       ( tyConArity )
 import DataCon
-import PrelNames   ( eqBoxDataConKey, coercibleDataConKey, unpackCStringIdKey
+import PrelNames   ( heqDataConKey, coercibleDataConKey, unpackCStringIdKey
                    , unpackCStringUtf8IdKey )
 import OptCoercion ( optCoercion )
 import PprCore     ( pprCoreBindings, pprRules )
@@ -93,7 +91,8 @@ import TysWiredIn
 ************************************************************************
 -}
 
--- | A substitution environment, containing both 'Id' and 'TyVar' substitutions.
+-- | A substitution environment, containing 'Id', 'TyVar', and 'CoVar'
+-- substitutions.
 --
 -- Some invariants apply to how you use the substitution:
 --
@@ -132,7 +131,7 @@ Note [Extending the Subst]
 For a core Subst, which binds Ids as well, we make a different choice for Ids
 than we do for TyVars.
 
-For TyVars, see Note [Extending the TvSubst] with Type.TvSubstEnv
+For TyVars, see Note [Extending the TCvSubst] with Type.TvSubstEnv
 
 For Ids, we have a different invariant
         The IdSubstEnv is extended *only* when the Unique on an Id changes
@@ -140,7 +139,7 @@ For Ids, we have a different invariant
 
 In consequence:
 
-* If the TvSubstEnv and IdSubstEnv are both empty, substExpr would be a
+* If all subst envs are empty, substExpr would be a
   no-op, so substExprSC ("short cut") does nothing.
 
   However, substExpr still goes ahead and substitutes.  Reason: we may
@@ -218,38 +217,48 @@ extendIdSubst (Subst in_scope ids tvs cvs) v r = Subst in_scope (extendVarEnv id
 extendIdSubstList :: Subst -> [(Id, CoreExpr)] -> Subst
 extendIdSubstList (Subst in_scope ids tvs cvs) prs = Subst in_scope (extendVarEnvList ids prs) tvs cvs
 
+-- | Add a substitution for a 'TyVar' to the 'Subst': the 'TyVar' *must*
+-- be a real TyVar, and not a CoVar
+extend_tv_subst :: Subst -> TyVar -> Type -> Subst
+extend_tv_subst (Subst in_scope ids tvs cvs) tv ty
+  = ASSERT( isTyVar tv )
+    Subst in_scope ids (extendVarEnv tvs tv ty) cvs
+
 -- | Add a substitution for a 'TyVar' to the 'Subst': you must ensure that the in-scope set is
 -- such that the "CoreSubst#in_scope_invariant" is true after extending the substitution like this
-extendTvSubst :: Subst -> TyVar -> Type -> Subst
-extendTvSubst (Subst in_scope ids tvs cvs) v r = Subst in_scope ids (extendVarEnv tvs v r) cvs
+extendTCvSubst :: Subst -> TyVar -> Type -> Subst
+extendTCvSubst subst v r
+  | isTyVar v
+  = extend_tv_subst subst v r
+  | Just co <- isCoercionTy_maybe r
+  = extendCvSubst subst v co
+  | otherwise
+  = pprPanic "CoreSubst.extendTCvSubst" (ppr v <+> ptext (sLit "|->") <+> ppr r)
 
--- | Adds multiple 'TyVar' substitutions to the 'Subst': see also 'extendTvSubst'
-extendTvSubstList :: Subst -> [(TyVar,Type)] -> Subst
-extendTvSubstList (Subst in_scope ids tvs cvs) prs = Subst in_scope ids (extendVarEnvList tvs prs) cvs
+-- | Adds multiple 'TyVar' substitutions to the 'Subst': see also 'extendTCvSubst'
+extendTCvSubstList :: Subst -> [(TyVar,Type)] -> Subst
+extendTCvSubstList subst vrs
+  = foldl' extend subst vrs
+  where extend subst (v, r) = extendTCvSubst subst v r
 
 -- | Add a substitution from a 'CoVar' to a 'Coercion' to the 'Subst': you must ensure that the in-scope set is
 -- such that the "CoreSubst#in_scope_invariant" is true after extending the substitution like this
 extendCvSubst :: Subst -> CoVar -> Coercion -> Subst
 extendCvSubst (Subst in_scope ids tvs cvs) v r = Subst in_scope ids tvs (extendVarEnv cvs v r)
 
--- | Adds multiple 'CoVar' -> 'Coercion' substitutions to the
--- 'Subst': see also 'extendCvSubst'
-extendCvSubstList :: Subst -> [(CoVar,Coercion)] -> Subst
-extendCvSubstList (Subst in_scope ids tvs cvs) prs = Subst in_scope ids tvs (extendVarEnvList cvs prs)
-
 -- | Add a substitution appropriate to the thing being substituted
 --   (whether an expression, type, or coercion). See also
---   'extendIdSubst', 'extendTvSubst', and 'extendCvSubst'.
+--   'extendIdSubst', 'extendTCvSubst'
 extendSubst :: Subst -> Var -> CoreArg -> Subst
 extendSubst subst var arg
   = case arg of
-      Type ty     -> ASSERT( isTyVar var ) extendTvSubst subst var ty
+      Type ty     -> ASSERT( isTyVar var ) extend_tv_subst subst var ty
       Coercion co -> ASSERT( isCoVar var ) extendCvSubst subst var co
       _           -> ASSERT( isId    var ) extendIdSubst subst var arg
 
 extendSubstWithVar :: Subst -> Var -> Var -> Subst
 extendSubstWithVar subst v1 v2
-  | isTyVar v1 = ASSERT( isTyVar v2 ) extendTvSubst subst v1 (mkTyVarTy v2)
+  | isTyVar v1 = ASSERT( isTyVar v2 ) extend_tv_subst subst v1 (mkTyVarTy v2)
   | isCoVar v1 = ASSERT( isCoVar v2 ) extendCvSubst subst v1 (mkCoVarCo v2)
   | otherwise  = ASSERT( isId    v2 ) extendIdSubst subst v1 (Var v2)
 
@@ -272,12 +281,12 @@ lookupIdSubst doc (Subst in_scope ids _ _) v
                 Var v
 
 -- | Find the substitution for a 'TyVar' in the 'Subst'
-lookupTvSubst :: Subst -> TyVar -> Type
-lookupTvSubst (Subst _ _ tvs _) v = ASSERT( isTyVar v) lookupVarEnv tvs v `orElse` Type.mkTyVarTy v
-
--- | Find the coercion substitution for a 'CoVar' in the 'Subst'
-lookupCvSubst :: Subst -> CoVar -> Coercion
-lookupCvSubst (Subst _ _ _ cvs) v = ASSERT( isCoVar v ) lookupVarEnv cvs v `orElse` mkCoVarCo v
+lookupTCvSubst :: Subst -> TyVar -> Type
+lookupTCvSubst (Subst _ _ tvs cvs) v
+  | isTyVar v
+  = lookupVarEnv tvs v `orElse` Type.mkTyVarTy v
+  | otherwise
+  = mkCoercionTy $ lookupVarEnv cvs v `orElse` mkCoVarCo v
 
 delBndr :: Subst -> Var -> Subst
 delBndr (Subst in_scope ids tvs cvs) v
@@ -487,8 +496,8 @@ substIdBndr _doc rec_subst subst@(Subst in_scope env tvs cvs) old_id
         | otherwise      = setIdType id1 (substTy subst old_ty)
 
     old_ty = idType old_id
-    no_type_change = isEmptyVarEnv tvs ||
-                     isEmptyVarSet (Type.tyVarsOfType old_ty)
+    no_type_change = (isEmptyVarEnv tvs && isEmptyVarEnv cvs) ||
+                     isEmptyVarSet (tyCoVarsOfType old_ty)
 
         -- new_id has the right IdInfo
         -- The lazy-set is because we're in a loop here, with
@@ -566,40 +575,37 @@ clone_id rec_subst subst@(Subst in_scope idvs tvs cvs) (old_id, uniq)
 
 For types and coercions we just call the corresponding functions in
 Type and Coercion, but we have to repackage the substitution, from a
-Subst to a TvSubst.
+Subst to a TCvSubst.
 -}
 
 substTyVarBndr :: Subst -> TyVar -> (Subst, TyVar)
 substTyVarBndr (Subst in_scope id_env tv_env cv_env) tv
-  = case Type.substTyVarBndr (TvSubst in_scope tv_env) tv of
-        (TvSubst in_scope' tv_env', tv')
-           -> (Subst in_scope' id_env tv_env' cv_env, tv')
+  = case Type.substTyVarBndr (TCvSubst in_scope tv_env cv_env) tv of
+        (TCvSubst in_scope' tv_env' cv_env', tv')
+           -> (Subst in_scope' id_env tv_env' cv_env', tv')
 
 cloneTyVarBndr :: Subst -> TyVar -> Unique -> (Subst, TyVar)
 cloneTyVarBndr (Subst in_scope id_env tv_env cv_env) tv uniq
-  = case Type.cloneTyVarBndr (TvSubst in_scope tv_env) tv uniq of
-        (TvSubst in_scope' tv_env', tv')
-           -> (Subst in_scope' id_env tv_env' cv_env, tv')
+  = case Type.cloneTyVarBndr (TCvSubst in_scope tv_env cv_env) tv uniq of
+        (TCvSubst in_scope' tv_env' cv_env', tv')
+           -> (Subst in_scope' id_env tv_env' cv_env', tv')
 
 substCoVarBndr :: Subst -> TyVar -> (Subst, TyVar)
 substCoVarBndr (Subst in_scope id_env tv_env cv_env) cv
-  = case Coercion.substCoVarBndr (CvSubst in_scope tv_env cv_env) cv of
-        (CvSubst in_scope' tv_env' cv_env', cv')
+  = case Coercion.substCoVarBndr (TCvSubst in_scope tv_env cv_env) cv of
+        (TCvSubst in_scope' tv_env' cv_env', cv')
            -> (Subst in_scope' id_env tv_env' cv_env', cv')
 
 -- | See 'Type.substTy'
 substTy :: Subst -> Type -> Type
-substTy subst ty = Type.substTy (getTvSubst subst) ty
-
-getTvSubst :: Subst -> TvSubst
-getTvSubst (Subst in_scope _ tenv _) = TvSubst in_scope tenv
+substTy subst ty = Type.substTy (getTCvSubst subst) ty
 
-getCvSubst :: Subst -> CvSubst
-getCvSubst (Subst in_scope _ tenv cenv) = CvSubst in_scope tenv cenv
+getTCvSubst :: Subst -> TCvSubst
+getTCvSubst (Subst in_scope _ tenv cenv) = TCvSubst in_scope tenv cenv
 
 -- | See 'Coercion.substCo'
 substCo :: Subst -> Coercion -> Coercion
-substCo subst co = Coercion.substCo (getCvSubst subst) co
+substCo subst co = Coercion.substCo (getTCvSubst subst) co
 
 {-
 ************************************************************************
@@ -611,9 +617,9 @@ substCo subst co = Coercion.substCo (getCvSubst subst) co
 
 substIdType :: Subst -> Id -> Id
 substIdType subst@(Subst _ _ tv_env cv_env) id
-  | (isEmptyVarEnv tv_env && isEmptyVarEnv cv_env) || isEmptyVarSet (Type.tyVarsOfType old_ty) = id
+  | (isEmptyVarEnv tv_env && isEmptyVarEnv cv_env) || isEmptyVarSet (tyCoVarsOfType old_ty) = id
   | otherwise   = setIdType id (substTy subst old_ty)
-                -- The tyVarsOfType is cheaper than it looks
+                -- The tyCoVarsOfType is cheaper than it looks
                 -- because we cache the free tyvars of the type
                 -- in a Note in the id's type itself
   where
@@ -728,7 +734,7 @@ substDVarSet subst fvs
   where
   subst_fv subst fv acc
      | isId fv = expr_fvs (lookupIdSubst (text "substDVarSet") subst fv) isLocalVar emptyVarSet $! acc
-     | otherwise = tyVarsOfTypeAcc (lookupTvSubst subst fv) (const True) emptyVarSet $! acc
+     | otherwise = tyCoVarsOfTypeAcc (lookupTCvSubst subst fv) (const True) emptyVarSet $! acc
 
 ------------------
 substTickish :: Subst -> Tickish Id -> Tickish Id
@@ -785,56 +791,67 @@ InlVanilla.  The WARN is just so I can see if it happens a lot.
 *                                                                      *
 ************************************************************************
 
-Note [Optimise coercion boxes aggressively]
+Note [Getting the map/coerce RULE to work]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We wish to allow the "map/coerce" RULE to fire:
 
-The simple expression optimiser needs to deal with Eq# boxes as follows:
- 1. If the result of optimising the RHS of a non-recursive binding is an
-    Eq# box, that box is substituted rather than turned into a let, just as
-    if it were trivial.
-       let eqv = Eq# co in e ==> e[Eq# co/eqv]
+  {-# RULES "map/coerce" map coerce = coerce #-}
 
- 2. If the result of optimising a case scrutinee is a Eq# box and the case
-    deconstructs it in a trivial way, we evaluate the case then and there.
-      case Eq# co of Eq# cov -> e ==> e[co/cov]
+The naive core produced for this is
 
-We do this for two reasons:
+  forall a b (dict :: Coercible * a b).
+    map @a @b (coerce @a @b @dict) = coerce @[a] @[b] @dict'
 
- 1. Bindings/case scrutinisation of this form is often created by the
-    evidence-binding mechanism and we need them to be inlined to be able
-    desugar RULE LHSes that involve equalities (see e.g. T2291)
+  where dict' :: Coercible [a] [b]
+        dict' = ...
 
- 2. The test T4356 fails Lint because it creates a coercion between types
-    of kind (* -> * -> *) and (?? -> ? -> *), which differ. If we do this
-    inlining aggressively we can collapse away the intermediate coercion between
-    these two types and hence pass Lint again. (This is a sort of a hack.)
+This matches literal uses of `map coerce` in code, but that's not what we
+want. We want it to match, say, `map MkAge` (where newtype Age = MkAge Int)
+too. Some of this is addressed by compulsorily unfolding coerce on the LHS,
+yielding
 
-In fact, our implementation uses slightly liberalised versions of the second rule
-rule so that the optimisations are a bit more generally applicable. Precisely:
- 2a. We reduce any situation where we can spot a case-