This project is mirrored from Pull mirroring failed .
Repository mirroring has been paused due to too many failed attempts. It can be resumed by a project maintainer.
Last successful update .
  1. 17 Dec, 2015 1 commit
  2. 11 Dec, 2015 1 commit
    •'s avatar
      Add kind equalities to GHC. · 67465497 authored
      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
       * 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.
  3. 25 Nov, 2015 1 commit
  4. 22 Apr, 2015 1 commit
  5. 02 Mar, 2015 1 commit
  6. 10 Feb, 2015 1 commit
  7. 16 Dec, 2014 1 commit
    • Peter Wortmann's avatar
      Source notes (Core support) · 993975d3
      Peter Wortmann authored
      This patch introduces "SourceNote" tickishs that link Core to the
      source code that generated it. The idea is to retain these source code
      links throughout code transformations so we can eventually relate
      object code all the way back to the original source (which we can,
      say, encode as DWARF information to allow debugging).  We generate
      these SourceNotes like other tickshs in the desugaring phase. The
      activating command line flag is "-g", consistent with the flag other
      compilers use to decide DWARF generation.
      Keeping ticks from getting into the way of Core transformations is
      tricky, but doable. The changes in this patch produce identical Core
      in all cases I tested -- which at this point is GHC, all libraries and
      nofib. Also note that this pass creates *lots* of tick nodes, which we
      reduce somewhat by removing duplicated and overlapping source
      ticks. This will still cause significant Tick "clumps" - a possible
      future optimization could be to make Tick carry a list of Tickishs
      instead of one at a time.
      (From Phabricator D169)
  8. 03 Dec, 2014 1 commit
  9. 26 Sep, 2014 1 commit
  10. 15 May, 2014 1 commit
    • Herbert Valerio Riedel's avatar
      Add LANGUAGE pragmas to compiler/ source files · 23892440
      Herbert Valerio Riedel authored
      In some cases, the layout of the LANGUAGE/OPTIONS_GHC lines has been
      reorganized, while following the convention, to
      - place `{-# LANGUAGE #-}` pragmas at the top of the source file, before
        any `{-# OPTIONS_GHC #-}`-lines.
      - Moreover, if the list of language extensions fit into a single
        `{-# LANGUAGE ... -#}`-line (shorter than 80 characters), keep it on one
        line. Otherwise split into `{-# LANGUAGE ... -#}`-lines for each
        individual language extension. In both cases, try to keep the
        enumeration alphabetically ordered.
        (The latter layout is preferable as it's more diff-friendly)
      While at it, this also replaces obsolete `{-# OPTIONS ... #-}` pragma
      occurences by `{-# OPTIONS_GHC ... #-}` pragmas.
  11. 24 Apr, 2014 1 commit
    • Simon Peyton Jones's avatar
      Don't eta-expand PAPs (fixes Trac #9020) · 79e46aea
      Simon Peyton Jones authored
      See Note [Do not eta-expand PAPs] in SimplUtils.  This has a tremendously
      good effect on compile times for some simple benchmarks.
      The test is now where it belongs, in perf/compiler/T9020 (instead of simpl015).
      I did a nofib run and got essentially zero change except for cacheprof which
      gets 4% more allocation.  I investigated.  Turns out that we have
          instance PP Reg where
             pp ppm ST_0 = "%st"
             pp ppm ST_1 = "%st(1)"
             pp ppm ST_2 = "%st(2)"
             pp ppm ST_3 = "%st(3)"
             pp ppm ST_4 = "%st(4)"
             pp ppm ST_5 = "%st(5)"
             pp ppm ST_6 = "%st(6)"
             pp ppm ST_7 = "%st(7)"
             pp ppm r    = "%" ++ map toLower (show r)
      That (map toLower (show r) does a lot of map/toLowers.  But if we inline show
      we get something like
             pp ppm ST_0 = "%st"
             pp ppm ST_1 = "%st(1)"
             pp ppm ST_2 = "%st(2)"
             pp ppm ST_3 = "%st(3)"
             pp ppm ST_4 = "%st(4)"
             pp ppm ST_5 = "%st(5)"
             pp ppm ST_6 = "%st(6)"
             pp ppm ST_7 = "%st(7)"
             pp ppm EAX  = map toLower (show EAX)
             pp ppm EBX  = map toLower (show EBX)
      and all those map/toLower calls can now be floated to top level.
      This gives a 4% decrease in allocation.  But it depends on inlining
      a pretty big 'show' function.
      With this new patch we get slightly better eta-expansion, which makes
      a function look slightly bigger, which just stops it being inlined.
      The previous behaviour was luck, so I'm not going to worry about
      losing it.
      I've added some notes to nofib/Simon-nofib-notes
  12. 11 Mar, 2014 1 commit
  13. 05 Mar, 2014 1 commit
  14. 17 Feb, 2014 1 commit
  15. 10 Feb, 2014 1 commit
    • Joachim Breitner's avatar
      Implement CallArity analysis · cdceadf3
      Joachim Breitner authored
      This analysis finds out if a let-bound expression with lower manifest
      arity than type arity is always called with more arguments, as in that
      case eta-expansion is allowed and often viable. The analysis is very
      much tailored towards the code generated when foldl is implemented via
      foldr; without this analysis doing so would be a very bad idea!
      There are other ways to improve foldr/builder-fusion to cope with foldl,
      if any of these are implemented then this step can probably be moved to
      -O2 to save some compilation times. The current impact of adding this
      phase is just below +2% (measured running GHC's "make").
  16. 12 Dec, 2013 1 commit
    • Simon Peyton Jones's avatar
      Improve the handling of used-once stuff · 80989de9
      Simon Peyton Jones authored
      Joachim and I are committing this onto a branch so that we can share it,
      but we expect to do a bit more work before merging it onto head.
      Nofib staus:
        - Most programs, no change
        - A few improve
        - A couple get worse (cacheprof, tak, rfib)
      Investigating the "get worse" set is what's holding up putting this
      on head.
      The major issue is this.  Consider
          map (f g) ys
      where f's demand signature looks like
         f :: <L,C1(C1(U))> -> <L,U> -> .
      So 'f' is not saturated.  What demand do we place on g?
      That is, the inner C1 should stay, even though f is not saturated.
      I found that this made a significant difference in the demand signatures
      inferred in GHC.IO, which uses lots of higher-order exception handlers.
      I also had to add used-once demand signatures for some of the
      'catch' primops, so that we know their handlers are only called once.
  17. 09 Dec, 2013 2 commits
    • Joachim Breitner's avatar
      Replace mkTopDmdType by mkClosedStrictSig · 3cdf1251
      Joachim Breitner authored
      because it is not a top deman (see previous commit), and it is only used
      in an argument to mkStrictSig.
    • Joachim Breitner's avatar
      Rename topDmdType to nopDmdType · f64cf134
      Joachim Breitner authored
      because topDmdType is ''not'' the top of the lattice, as it puts an
      implicit absent demand on free variables, but Abs is the bottom of the
      Usage lattice.
      Why nopDmdType? Becuase it is the demand of doing nothing: Everything
      lazy, everything absent, no definite divergence.
  18. 12 Nov, 2013 1 commit
    • Simon Peyton Jones's avatar
      Improve eta expansion (again) · 802f4b89
      Simon Peyton Jones authored
      The presenting issue was that we were never eta-expanding
          f (\x -> case x of (a,b) -> \s -> blah)
      and that meant we were allocating two lambdas instead of one.
      See Note [Eta expanding lambdas] in SimplUtils.
      However I didn't want to eta expand the lambda, and then try all over
      again for tryEtaExpandRhs.  Yet the latter is important in the context
      of a let-binding it can do simple arity analysis.  So I ended up
      refactoring CallCtxt so that it tells when we are on the RHS of a let.
      I also moved findRhsArity from SimplUtils to CoreArity.
      Performance increases nicely. Here are the ones where allocation improved
      by more than 0.5%. Notice the nice decrease in binary size too.
              Program           Size    Allocs   Runtime   Elapsed  TotalMem
                 ansi          -2.3%     -0.9%      0.00      0.00     +0.0%
                 bspt          -2.1%     -9.7%      0.01      0.01    -33.3%
                fasta          -1.8%    -11.7%     -3.4%     -3.6%     +0.0%
                  fft          -1.9%     -1.3%      0.06      0.06    +11.1%
      reverse-complem          -1.9%    -18.1%     -1.9%     -2.8%     +0.0%
               sphere          -1.8%     -4.5%      0.09      0.09     +0.0%
            transform          -1.8%     -2.3%     -4.6%     -3.1%     +0.0%
                  Min          -3.0%    -18.1%    -13.9%    -14.6%    -35.7%
                  Max          -1.3%     +0.0%     +7.7%     +7.7%    +50.0%
       Geometric Mean          -1.9%     -0.6%     -2.1%     -2.1%     -0.2%
  19. 24 Oct, 2013 1 commit
    • Simon Peyton Jones's avatar
      Refactor the topNormaliseNewType story, fixing Trac #8467 · 2650da2b
      Simon Peyton Jones authored
      A bit of a mess had accumulated, with unclear invariants.
      * Remove splitNewTypeRepCo_maybe, in favour of topNormaliseNewType_maybe
        (which had the same signature but behaved subtly differently).
      * Make topNormaliseNewType_maybe guaranteed to return a non-newtype
        if it says (Just ty).  This is what was causing the loop in #8467
      * Apply similar tidying up to FamInstEnv.topNormaliseType
  20. 08 Oct, 2013 1 commit
  21. 01 Oct, 2013 1 commit
  22. 06 Jun, 2013 1 commit
    • Simon Peyton Jones's avatar
      Add TyCon.checkRecTc, and use in in typeArity · a1a67b58
      Simon Peyton Jones authored
      This just formalises an abstraction we've been using anyway,
      namely to expand "recursive" TyCons until we see them twice.
      We weren't doing this in typeArity, and that inconsistency
      was leading to a subsequent ASSERT failure, when compiling
      Stream.hs, which has a newtype like this
         newtype Stream m a b = Stream (m (Either b (a, Stream m a b)))
  23. 30 Jan, 2013 1 commit
  24. 17 Jan, 2013 1 commit
    • Simon Peyton Jones's avatar
      Major patch to implement the new Demand Analyser · 0831a12e
      Simon Peyton Jones authored
      This patch is the result of Ilya Sergey's internship at MSR.  It
      constitutes a thorough overhaul and simplification of the demand
      analyser.  It makes a solid foundation on which we can now build.
      Main changes are
      * Instead of having one combined type for Demand, a Demand is
         now a pair (JointDmd) of
            - a StrDmd and
            - an AbsDmd.
         This allows strictness and absence to be though about quite
         orthogonally, and greatly reduces brain melt-down.
      * Similarly in the DmdResult type, it's a pair of
           - a PureResult (indicating only divergence/non-divergence)
           - a CPRResult (which deals only with the CPR property
      * In IdInfo, the
          strictnessInfo field contains a StrictSig, not a Maybe StrictSig
          demandInfo     field contains a Demand, not a Maybe Demand
        We don't need Nothing (to indicate no strictness/demand info)
        any more; topSig/topDmd will do.
      * Remove "boxity" analysis entirely.  This was an attempt to
        avoid "reboxing", but it added complexity, is extremely
        ad-hoc, and makes very little difference in practice.
      * Remove the "unboxing strategy" computation. This was an an
        attempt to ensure that a worker didn't get zillions of
        arguments by unboxing big tuples.  But in fact removing it
        DRAMATICALLY reduces allocation in an inner loop of the
        I/O library (where the threshold argument-count had been
        set just too low).  It's exceptional to have a zillion arguments
        and I don't think it's worth the complexity, especially since
        it turned out to have a serious performance hit.
      * Remove quite a bit of ad-hoc cruft
      * Move worthSplittingFun, worthSplittingThunk from WorkWrap to
        Demand. This allows JointDmd to be fully abstract, examined
        only inside Demand.
      Everything else really follows from these changes.
      All of this is really just refactoring, so we don't expect
      big performance changes, but acutally the numbers look quite
      good.  Here is a full nofib run with some highlights identified:
              Program           Size    Allocs   Runtime   Elapsed  TotalMem
               expert          -2.6%    -15.5%      0.00      0.00     +0.0%
                fluid          -2.4%     -7.1%      0.01      0.01     +0.0%
                   gg          -2.5%    -28.9%      0.02      0.02    -33.3%
            integrate          -2.6%     +3.2%     +2.6%     +2.6%     +0.0%
              mandel2          -2.6%     +4.2%      0.01      0.01     +0.0%
             nucleic2          -2.0%    -16.3%      0.11      0.11     +0.0%
                 para          -2.6%    -20.0%    -11.8%    -11.7%     +0.0%
               parser          -2.5%    -17.9%      0.05      0.05     +0.0%
               prolog          -2.6%    -13.0%      0.00      0.00     +0.0%
               puzzle          -2.6%     +2.2%     +0.8%     +0.8%     +0.0%
              sorting          -2.6%    -35.9%      0.00      0.00     +0.0%
             treejoin          -2.6%    -52.2%     -9.8%     -9.9%     +0.0%
                  Min          -2.7%    -52.2%    -11.8%    -11.7%    -33.3%
                  Max          -1.8%     +4.2%    +10.5%    +10.5%     +7.7%
       Geometric Mean          -2.5%     -2.8%     -0.4%     -0.5%     -0.4%
      Things to note
      * Binary sizes are smaller. I don't know why, but it's good.
      * Allocation is sometiemes a *lot* smaller. I believe that all the big numbers
        (I checked treejoin, gg, sorting) arise from one place, namely a function
        GHC.IO.Encoding.UTF8.utf8_decode, which is strict in two Buffers both of
        which have several arugments.  Not w/w'ing both arguments (which is what
        we did before) has a big effect.  So the big win in actually somewhat
        accidental, gained by removing the "unboxing strategy" code.
      * A couple of benchmarks allocate slightly more.  This turns out
        to be due to reboxing (integrate).  But the biggest increase is
        mandel2, and *that* turned out also to be a somewhat accidental
        loss of CSE, and pointed the way to doing better CSE: see Trac
      * Runtimes are never very reliable, but seem to improve very slightly.
      All in all, a good piece of work.  Thank you Ilya!
  25. 16 Oct, 2012 2 commits
  26. 02 May, 2012 1 commit
    • Simon Peyton Jones's avatar
      Allow cases with empty alterantives · ac230c5e
      Simon Peyton Jones authored
      This patch allows, for the first time, case expressions with an empty
      list of alternatives. Max suggested the idea, and Trac #6067 showed
      that it is really quite important.
      So I've implemented the idea, fixing #6067. Main changes
       * See Note [Empty case alternatives] in CoreSyn
       * Various foldr1's become foldrs
       * IfaceCase does not record the type of the alternatives.
         I added IfaceECase for empty-alternative cases.
       * Core Lint does not complain about empty cases
       * MkCore.castBottomExpr constructs an empty-alternative case
         expression   (case e of ty {})
       * CoreToStg converts '(case e of {})' to just 'e'
  27. 27 Apr, 2012 2 commits
    • Simon Peyton Jones's avatar
      Revert "Refactoring in CoreUtils/CoreArity" · a2ae0d77
      Simon Peyton Jones authored
      This reverts commit e3f8557c.
      Sigh. Seg fault.
    • Simon Peyton Jones's avatar
      Refactoring in CoreUtils/CoreArity · e3f8557c
      Simon Peyton Jones authored
      In the previous commit about "aggressive primops" I wanted a new
      function CoreUtils.exprCertainlyTerminates.  In doing this I ended up
      with a significant refactoring in CoreUtils.  The new structure has
      quite a lot of nice sharing:
               exprIsCheap             = exprIsCheap' isHNFApp
               exprIsExpandable        = exprIsCheap' isConLikeApp
               exprIsHNF               = exprIsHNFlike isHNFApp
               exprIsConLike           = exprIsHNFlike isConLikeApp
               exprCertainlyTerminates = exprIsHNFlike isTerminatingApp
      This patch also does some renaming
          CheapAppFun      -->   FunAppAnalyser
          isCheapApp       -->   isHNFApp
          isExpandableApp  -->   isConLikeApp
  28. 16 Jan, 2012 1 commit
  29. 13 Jan, 2012 1 commit
    • Simon Peyton Jones's avatar
      Add -faggressive-primops plus refactoring in CoreUtils · 601c983d
      Simon Peyton Jones authored
      I'm experimenting with making GHC a bit more aggressive about
        a) dropping case expressions if the result is unused
              Simplify.rebuildCase, CaseElim equation
        b) floating case expressions inwards
              FloatIn.fiExpr, AnnCase
      In both cases the new behaviour is gotten with a static (debug)
      flag -faggressive-primops.  The extra "aggression" is to allow
      discarding and floating in for side-effecting operations.  See
      the new, extensive Note [PrimOp can_fail and has_side_effects]
      in PrimoOp.
      When discarding a case with unused binders, in the lifted-type
      case it's definitely ok if the scrutinee terminates; previously
      we were checking exprOkForSpeculation, which is significantly
      So I wanted a new function CoreUtils.exprCertainlyTerminates.
      In doing this I ended up with a significant refactoring in
      CoreUtils.  The new structure has quite a lot of nice sharing:
          exprIsCheap             = exprIsCheap' isHNFApp
          exprIsExpandable        = exprIsCheap' isConLikeApp
          exprIsHNF               = exprIsHNFlike isHNFApp
          exprIsConLike           = exprIsHNFlike isConLikeApp
          exprCertainlyTerminates = exprIsHNFlike isTerminatingApp
  30. 16 Nov, 2011 1 commit
  31. 11 Nov, 2011 1 commit
    • Simon Peyton Jones's avatar
      Tighten up the definition of arityType a bit further, · a522c3b2
      Simon Peyton Jones authored
      to make Trac #5625 work.  The main change is that
      we eta-expand (case x of p -> \y. blah) only if the
      case-expression is in the context of a \x.  That is still
      technically unsound, but it makes a big difference to
      performance; and the change narrows the unsound cases
      a lot.
  32. 09 Nov, 2011 1 commit
    • Simon Peyton Jones's avatar
      Fix Trac #5475: another bug in exprArity · b8abb31f
      Simon Peyton Jones authored
      As usual it was to do with the handling of bottoms,
      but this time it wasn't terribly subtle; I was using
      andArityType (which is designed for case branches) as
      a cheap short cut for the arity trimming needed with
      a cast.  That did the Wrong Thing for bottoming
      expressions.  Sigh.
  33. 04 Nov, 2011 1 commit
  34. 02 Nov, 2011 1 commit
    • Simon Marlow's avatar
      Overhaul of infrastructure for profiling, coverage (HPC) and breakpoints · 7bb0447d
      Simon Marlow authored
      User visible changes
      Flags renamed (the old ones are still accepted for now):
        OLD            NEW
        ---------      ------------
        -auto-all      -fprof-auto
        -auto          -fprof-exported
        -caf-all       -fprof-cafs
      New flags:
        -fprof-auto              Annotates all bindings (not just top-level
                                 ones) with SCCs
        -fprof-top               Annotates just top-level bindings with SCCs
        -fprof-exported          Annotates just exported bindings with SCCs
        -fprof-no-count-entries  Do not maintain entry counts when profiling
                                 (can make profiled code go faster; useful with
                                 heap profiling where entry counts are not used)
      Cost-centre stacks have a new semantics, which should in most cases
      result in more useful and intuitive profiles.  If you find this not to
      be the case, please let me know.  This is the area where I have been
      experimenting most, and the current solution is probably not the
      final version, however it does address all the outstanding bugs and
      seems to be better than GHC 7.2.
      Stack traces
      +RTS -xc now gives more information.  If the exception originates from
      a CAF (as is common, because GHC tends to lift exceptions out to the
      top-level), then the RTS walks up the stack and reports the stack in
      the enclosing update frame(s).
      Result: +RTS -xc is much more useful now - but you still have to
      compile for profiling to get it.  I've played around a little with
      adding 'head []' to GHC itself, and +RTS -xc does pinpoint the problem
      quite accurately.
      I plan to add more facilities for stack tracing (e.g. in GHCi) in the
      Coverage (HPC)
       * derived instances are now coloured yellow if they weren't used
       * likewise record field names
       * entry counts are more accurate (hpc --fun-entry-count)
       * tab width is now correct (markup was previously off in source with
      Internal changes
      In Core, the Note constructor has been replaced by
              Tick (Tickish b) (Expr b)
      which is used to represent all the kinds of source annotation we
      support: profiling SCCs, HPC ticks, and GHCi breakpoints.
      Depending on the properties of the Tickish, different transformations
      apply to Tick.  See CoreUtils.mkTick for details.
      This commit closes the following tickets, test cases to follow:
        - Close #2552: not a bug, but the behaviour is now more intuitive
          (test is T2552)
        - Close #680 (test is T680)
        - Close #1531 (test is result001)
        - Close #949 (test is T949)
        - Close #2466: test case has bitrotted (doesn't compile against current
          version of vector-space package)
  35. 21 Oct, 2011 1 commit
    • Simon Peyton Jones's avatar
      Be even more careful about eta expansion when bottom is involved · 6d5dfbf7
      Simon Peyton Jones authored
      See Note [Dealing with bottom], reproduced below.  Fixes Trac #5557.
      3.  Note [Dealing with bottom]
      	f = \x -> error "foo"
      Here, arity 1 is fine.  But if it is
      	f = \x -> case x of
      			True  -> error "foo"
      			False -> \y -> x+y
      then we want to get arity 2.  Technically, this isn't quite right, because
      	(f True) `seq` 1
      should diverge, but it'll converge if we eta-expand f.  Nevertheless, we
      do so; it improves some programs significantly, and increasing convergence
      isn't a bad thing.  Hence the ABot/ATop in ArityType.
      However, this really isn't always the Right Thing, and we have several
      tickets reporting unexpected bahaviour resulting from this
      transformation.  So we try to limit it as much as possible:
       * Do NOT move a lambda outside a known-bottom case expression
            case undefined of { (a,b) -> \y -> e }
         This showed up in Trac #5557
       * Do NOT move a lambda outside a case if all the branches of
         the case are known to return bottom.
            case x of { (a,b) -> \y -> error "urk" }
         This case is less important, but the idea is that if the fn is
         going to diverge eventually anyway then getting the best arity
         isn't an issue, so we might as well play safe
      Of course both these are readily defeated by disguising the bottoms.
  36. 09 Sep, 2011 1 commit
    • Simon Peyton Jones's avatar
      Obey the exprArity invariants! Fixes Trac #5441 · 1466b0ca
      Simon Peyton Jones authored
      We were giving arity 2 to a function whose type was
          Int -> Any
      That contradicts the exprArity invariant
      (see Note [exprArity invariant] in CoreArity), and
      in turn led to function whose actually code-generated arity
      was different that advertised in the interface file.
      Result: seg-fault city.
  37. 19 Apr, 2011 1 commit
    • Simon Peyton Jones's avatar
      This BIG PATCH contains most of the work for the New Coercion Representation · fdf86568
      Simon Peyton Jones authored
      See the paper "Practical aspects of evidence based compilation in System FC"
      * Coercion becomes a data type, distinct from Type
      * Coercions become value-level things, rather than type-level things,
        (although the value is zero bits wide, like the State token)
        A consequence is that a coerion abstraction increases the arity by 1
        (just like a dictionary abstraction)
      * There is a new constructor in CoreExpr, namely Coercion, to inject
        coercions into terms