GitLab

This commit implements the proposal in
https://github.com/ghc-proposals/ghc-proposals/pull/29 and
https://github.com/ghc-proposals/ghc-proposals/pull/35.

Here are some of the pieces of that proposal:

* Some of RuntimeRep's constructors have been shortened.

* TupleRep and SumRep are now parameterized over a list of RuntimeReps.
* This
means that two types with the same kind surely have the same
representation.
Previously, all unboxed tuples had the same kind, and thus the fact
above was
false.

* RepType.typePrimRep and friends now return a *list* of PrimReps. These
functions can now work successfully on unboxed tuples. This change is
necessary because we allow abstraction over unboxed tuple types and so
cannot
always handle unboxed tuples specially as we did before.

* We sometimes have to create an Id from a PrimRep. I thus split PtrRep
* into
LiftedRep and UnliftedRep, so that the created Ids have the right
strictness.

* The RepType.RepType type was removed, as it didn't seem to help with
* much.

* The RepType.repType function is also removed, in favor of typePrimRep.

* I have waffled a good deal on whether or not to keep VoidRep in
TyCon.PrimRep. In the end, I decided to keep it there. PrimRep is *not*
represented in RuntimeRep, and typePrimRep will never return a list
including
VoidRep. But it's handy to have in, e.g., ByteCodeGen and friends. I can
imagine another design choice where we have a PrimRepV type that is
PrimRep
with an extra constructor. That seemed to be a heavier design, though,
and I'm
not sure what the benefit would be.

* The last, unused vestiges of # (unliftedTypeKind) have been removed.

* There were several pretty-printing bugs that this change exposed;
* these are fixed.

* We previously checked for levity polymorphism in the types of binders.
* But we
also must exclude levity polymorphism in function arguments. This is
hard to check
for, requiring a good deal of care in the desugarer. See Note [Levity
polymorphism
checking] in DsMonad.

* In order to efficiently check for levity polymorphism in functions, it
* was necessary
to add a new bit of IdInfo. See Note [Levity info] in IdInfo.

* It is now safe for unlifted types to be unsaturated in Core. Core Lint
* is updated
accordingly.

* We can only know strictness after zonking, so several checks around
* strictness
in the type-checker (checkStrictBinds, the check for unlifted variables
under a ~
pattern) have been moved to the desugarer.

* Along the way, I improved the treatment of unlifted vs. banged
* bindings. See
Note [Strict binds checks] in DsBinds and #13075.

* Now that we print type-checked source, we must be careful to print
* ConLikes correctly.
This is facilitated by a new HsConLikeOut constructor to HsExpr.
Particularly troublesome
are unlifted pattern synonyms that get an extra void# argument.

* Includes a submodule update for haddock, getting rid of #.

* New testcases:
  typecheck/should_fail/StrictBinds
  typecheck/should_fail/T12973
  typecheck/should_run/StrictPats
  typecheck/should_run/T12809
  typecheck/should_fail/T13105
  patsyn/should_fail/UnliftedPSBind
  typecheck/should_fail/LevPolyBounded
  typecheck/should_compile/T12987
  typecheck/should_compile/T11736

* Fixed tickets:
  #12809
  #12973
  #11736
  #13075
  #12987

* This also adds a test case for #13105. This test case is
* "compile_fail" and
succeeds, because I want the testsuite to monitor the error message.
When #13105 is fixed, the test case will compile cleanly.

While investigating something else I found that 'typeSize' was
allocating like crazy.  Stupid becuase it should allocate precisely
nothing!!

Turned out that it was because typeSize and coercionSize were mutually
recursive across module boundaries, and so could not benefit from the
CPR property.  To fix this I moved them both into TyCoRep.

It's not critical (because typeSize is really only used in
debug mode, but I tripped over and example (T5642) in which
typeSize was one of the biggest single allocators in all of GHC.
And it's easy to fix, so I did.

Previously, GHC checked for bad levity polymorphism to the left of all
arrows in data constructors. This was wrong, as reported in #12911
(where an example is also shown). The solution is to check each
individual argument for bad levity polymorphism.  Thus the check has
been moved from TcValidity to TcTyClsDecls.

A similar situation exists with pattern synonyms, also fixed here.

This patch also nabs #12819 while I was in town.

Test cases: typecheck/should_compile/T12911, patsyn/should_fail/T12819

Test Plan: ./validate

Reviewers: simonpj, austin, bgamari

Reviewed By: bgamari

Subscribers: thomie

Differential Revision: https://phabricator.haskell.org/D2783

GHC Trac Issues: #12819, #12911

Summary:
Previously, we tested for type synonym loops by doing
a syntactic test on the literal type synonym declarations.
However, in some cases, loops could go through hs-boot
files, leading to an infinite loop (#12042); a similar
situation can occur when signature merging.

This commit replaces the syntactic test with a test on
TyCon, simply by walking down all type synonyms until
we bottom out, or find we've looped back.  It's a lot
simpler.
Signed-off-by: Edward Z. Yang <ezyang@cs.stanford.edu>

Test Plan: validate

Reviewers: simonpj, austin, bgamari

Subscribers: goldfire, thomie

Differential Revision: https://phabricator.haskell.org/D2656

GHC Trac Issues: #12042

Here we consolidate the pretty-printing logic for types in IfaceType. We
need IfaceType regardless and the printer for Type can be implemented in
terms of that for IfaceType. See #11660.

Note that this is very much a work-in-progress. Namely I still have yet
to ponder how to ease the hs-boot file situation, still need to rip out
more dead code, need to move some of the special cases for, e.g., `*` to
the IfaceType printer, and need to get it to validate. That being said,
it comes close to validating as-is.

Test Plan: Validate

Reviewers: goldfire, austin

Subscribers: goldfire, thomie, simonpj

Differential Revision: https://phabricator.haskell.org/D2528

GHC Trac Issues: #11660

This patch does two related things

* Combines the occurrence-check logic in the on-the-fly unifier with
  that in the constraint solver.  They are both doing the same job,
  after all.  The resulting code is now in TcUnify:
     metaTyVarUpdateOK
     occCheckExpand
     occCheckForErrors (called in TcErrors)

* In doing this I disovered checking for family-free-ness and foralls
  can be unnecessarily inefficient, because it expands type synonyms.
  It's easy just to cache this info in the type syononym TyCon, which
  I am now doing.

This patch does a raft of useful tidy-ups in the type checker.
I've been meaning to do this for some time, and finally made
time to do it en route to ICFP.

1. Modify TcType.ExpType to make a distinct data type,
   InferResult for the Infer case, and consequential
   refactoring.

2. Define a new function TcUnify.fillInferResult, to fill in
   an InferResult. It uses TcMType.promoteTcType to promote
   the type to the level of the InferResult.
   See TcMType Note [Promoting a type]
   This refactoring is in preparation for an improvement
   to typechecking pattern bindings, coming next.

   I flirted with an elaborate scheme to give better
   higher rank inference, but it was just too complicated.
   See TcMType Note [Promotion and higher rank types]

3. Add to InferResult a new field ir_inst :: Bool to say
   whether or not the type used to fill in the
   InferResult should be deeply instantiated.  See
   TcUnify Note [Deep instantiation of InferResult].

4. Add a TcLevel to SkolemTvs. This will be useful generally

    - it's a fast way to see if the type
      variable escapes when floating (not used yet)

    - it provides a good consistency check when updating a
      unification variable (TcMType.writeMetaTyVarRef, the
      level_check_ok check)

   I originally had another reason (related to the flirting
   in (2), but I left it in because it seems like a step in
   the right direction.

5. Reduce and simplify the plethora of uExpType,
   tcSubType and related functions in TcUnify.  It was
   such an opaque mess and it's still not great, but it's
   better.

6. Simplify the uo_expected field of TypeEqOrigin.  Richard
   had generatlised it to a ExpType, but it was almost always
   a Check type.  Now it's back to being a plain TcType which
   is much, much easier.

7. Improve error messages by refraining from skolemisation when
   it's clear that there's an error: see
   TcUnify Note [Don't skolemise unnecessarily]

8. Type.isPiTy and isForAllTy seem to be missing a coreView check,
   so I added it

9. Kill off tcs_used_tcvs.  Its purpose is to track the
   givens used by wanted constraints.  For dictionaries etc
   we do that via the free vars of the /bindings/ in the
   implication constraint ic_binds.  But for coercions we
   just do update-in-place in the type, rather than
   generating a binding.  So we need something analogous to
   bindings, to track what coercions we have added.

   That was the purpose of tcs_used_tcvs.  But it only
   worked for a /single/ iteration, whereas we may have
   multiple iterations of solving an implication.  Look
   at (the old) 'setImplicationStatus'.  If the constraint
   is unsolved, it just drops the used_tvs on the floor.
   If it becomes solved next time round, we'll pick up
   coercions used in that round, but ignore ones used in
   the first round.

   There was an outright bug.  Result = (potentialy) bogus
   unused-constraint errors.  Constructing a case where this
   actually happens seems quite trick so I did not do so.

   Solution: expand EvBindsVar to include the (free vars of
   the) coercions, so that the coercions are tracked in
   essentially the same way as the bindings.

   This turned out to be much simpler.  Less code, more
   correct.

10. Make the ic_binds field in an implication have type
      ic_binds :: EvBindsVar
    instead of (as previously)
       ic_binds :: Maybe EvBindsVar
    This is notably simpler, and faster to use -- less
    testing of the Maybe.  But in the occaional situation
    where we don't have anywhere to put the bindings, the
    belt-and-braces error check is lost.  So I put it back
    as an ASSERT in 'setImplicationStatus' (see the use of
    'termEvidenceAllowed')

All these changes led to quite bit of error message wibbling

Summary:
This patch implements primitive unboxed sum types, as described in
https://ghc.haskell.org/trac/ghc/wiki/UnpackedSumTypes.

Main changes are:

- Add new syntax for unboxed sums types, terms and patterns. Hidden
  behind `-XUnboxedSums`.

- Add unlifted unboxed sum type constructors and data constructors,
  extend type and pattern checkers and desugarer.

- Add new RuntimeRep for unboxed sums.

- Extend unarise pass to translate unboxed sums to unboxed tuples right
  before code generation.

- Add `StgRubbishArg` to `StgArg`, and a new type `CmmArg` for better
  code generation when sum values are involved.

- Add user manual section for unboxed sums.

Some other changes:

- Generalize `UbxTupleRep` to `MultiRep` and `UbxTupAlt` to
  `MultiValAlt` to be able to use those with both sums and tuples.

- Don't use `tyConPrimRep` in `isVoidTy`: `tyConPrimRep` is really
  wrong, given an `Any` `TyCon`, there's no way to tell what its kind
  is, but `kindPrimRep` and in turn `tyConPrimRep` returns `PtrRep`.

- Fix some bugs on the way: #12375.

Not included in this patch:

- Update Haddock for new the new unboxed sum syntax.

- `TemplateHaskell` support is left as future work.

For reviewers:

- Front-end code is mostly trivial and adapted from unboxed tuple code
  for type checking, pattern checking, renaming, desugaring etc.

- Main translation routines are in `RepType` and `UnariseStg`.
  Documentation in `UnariseStg` should be enough for understanding
  what's going on.

Credits:

- Johan Tibell wrote the initial front-end and interface file
  extensions.

- Simon Peyton Jones reviewed this patch many times, wrote some code,
  and helped with debugging.

Reviewers: bgamari, alanz, goldfire, RyanGlScott, simonpj, austin,
           simonmar, hvr, erikd

Reviewed By: simonpj

Subscribers: Iceland_jack, ggreif, ezyang, RyanGlScott, goldfire,
             thomie, mpickering

Differential Revision: https://phabricator.haskell.org/D2259

This removes an unnecessary loop looking for invisible binders
and tries to clarify what the very closely-related functions
tcInferArgs, tc_infer_args, tcInferApps all do.

This renames VisibilityFlag from

> data VisibilityFlag = Visible | Specified | Invisible

to

> data ArgFlag = Required | Specified | Inferred

The old name was quite confusing, because both Specified
and Invisible were invisible! The new names are hopefully clearer.

Very minor

We want to remove the `Ord Unique` instance because there's
no way to implement it in deterministic way and it's too
easy to use by accident.

We sometimes compute SCC for datatypes whose Ord instance
is implemented in terms of Unique. The Ord constraint on
SCC is just an artifact of some internal data structures.
We can have an alternative implementation with a data
structure that uses Uniquable instead.

This does exactly that and I'm pleased that I didn't have
to introduce any duplication to do that.

Test Plan:
./validate
I looked at performance tests and it's a tiny bit better.

Reviewers: bgamari, simonmar, ezyang, austin, goldfire

Subscribers: thomie

Differential Revision: https://phabricator.haskell.org/D2359

GHC Trac Issues: #4012

Before this patch, following the TypeInType innovations,
each TyCon had two lists:
  - tyConBinders :: [TyBinder]
  - tyConTyVars  :: [TyVar]

They were in 1-1 correspondence and contained
overlapping information.  More broadly, there were many
places where we had to pass around this pair of lists,
instead of a single list.

This commit tidies all that up, by having just one list of
binders in a TyCon:

  - tyConBinders :: [TyConBinder]

The new data types look like this:

  Var.hs:
     data TyVarBndr tyvar vis = TvBndr tyvar vis
     data VisibilityFlag = Visible | Specified | Invisible
     type TyVarBinder = TyVarBndr TyVar VisibilityFlag

  TyCon.hs:
     type TyConBinder = TyVarBndr TyVar TyConBndrVis

     data TyConBndrVis
       = NamedTCB VisibilityFlag
       | AnonTCB

  TyCoRep.hs:
     data TyBinder
       = Named TyVarBinder
       | Anon Type

Note that Var.TyVarBdr has moved from TyCoRep and has been
made polymorphic in the tyvar and visiblity fields:

     type TyVarBinder = TyVarBndr TyVar VisibilityFlag
        -- Used in ForAllTy
     type TyConBinder = TyVarBndr TyVar TyConBndrVis
        -- Used in TyCon

     type IfaceForAllBndr  = TyVarBndr IfaceTvBndr VisibilityFlag
     type IfaceTyConBinder = TyVarBndr IfaceTvBndr TyConBndrVis
         -- Ditto, in interface files

There are a zillion knock-on changes, but everything
arises from these types.  It was a bit fiddly to get the
module loops to work out right!

Some smaller points
~~~~~~~~~~~~~~~~~~~
* Nice new functions
    TysPrim.mkTemplateKiTyVars
    TysPrim.mkTemplateTyConBinders
  which help you make the tyvar binders for dependently-typed
  TyCons.  See comments with their definition.

* The change showed up a bug in TcGenGenerics.tc_mkRepTy, where the code
  was making an assumption about the order of the kind variables in the
  kind of GHC.Generics.(:.:).  I fixed this; see TcGenGenerics.mkComp.

With TypeInType Richard combined ForAllTy and FunTy, but that was often
awkward, and yielded little benefit becuase in practice the two were
always treated separately.  This patch re-introduces FunTy.  Specfically

* New type
    data TyVarBinder = TvBndr TyVar VisibilityFlag
  This /always/ has a TyVar it.  In many places that's just what
  what we want, so there are /lots/ of TyBinder -> TyVarBinder changes

* TyBinder still exists:
    data TyBinder = Named TyVarBinder | Anon Type

* data Type = ForAllTy TyVarBinder Type
            | FunTy Type Type
            |  ....

There are a LOT of knock-on changes, but they are all routine.

The Haddock submodule needs to be updated too

This makes it obvious that it's nondeterministic and hopefully
will prevent someone from using it accidentally.

GHC Trac: #4012

isPredTy can be called on ill-kinded types, especially (of course) if
there is a kind error.  We don't wnat it to crash, but it was, in
piResultTy.

This patch introduces piResultTy_maybe, and uses it in isPredTy.

Ugh.  I dislike this code.  It's mainly used to know when we should
print types with '=>', and we should probably have a better way to
signal that.

...about unarisation and unboxed tuples

This is a continuation of
   commit e9e61f18
   Date:   Thu May 26 15:24:53 2016 +0100
   Reduce special-casing for nullary unboxed tuple

which related to Trac #12115.  But typecheck/should_run/tcrun051
revealed that my patch was incomplete.

This fixes it, by removing another special case in Type.repType.
I had also missed a case in UnariseStg.unariseIdBinder.

I took the opportunity to add explanatory notes
  Note [Unarisation]
  Note [Unarisation and nullary tuples]
in UnariseStg

When we built the kind of a nullary unboxed tuple, we said, in
TysWiredIn.mk_tuple:

    res_rep | arity == 0 = voidRepDataConTy
                  -- See Note [Nullary unboxed tuple] in Type
            | otherwise  = unboxedTupleRepDataConTy

But this is bogus.  The Note deals with what the 'unarise' transformation
does, and up to that point it's simpler and more uniform to treat
nullary unboxed tuples the same as all the others.

Nicer now.  And it fixes the Lint error in Trac #12115

When `deriveTyData` attempts to unify two kind variables (which can
happen if both the typeclass and the datatype are poly-kinded), it
mistakenly adds an extra mapping to its substitution which causes the
unification to fail when applying the substitution. This can be
prevented by checking both the domain and the range of the original
substitution to see which kind variables shouldn't be put into the
domain of the substitution. A more in-depth explanation is included in
`Note [Unification of two kind variables in deriving]`.

Fixes #11837.

Test Plan: ./validate

Reviewers: simonpj, hvr, goldfire, niteria, austin, bgamari

Reviewed By: bgamari

Subscribers: niteria, thomie

Differential Revision: https://phabricator.haskell.org/D2117

GHC Trac Issues: #11837

simplifyInstanceContexts used cmpType which is nondeterministic
for canonicalising typeclass constraints in derived instances.
Following changes make it deterministic as explained by the
Note [Deterministic simplifyInstanceContexts].

Test Plan: ./validate

Reviewers: simonmar, goldfire, simonpj, austin, bgamari

Reviewed By: simonpj

Subscribers: thomie

Differential Revision: https://phabricator.haskell.org/D2173

GHC Trac Issues: #4012

varSetElemsWellScoped introduces unnecessary non-determinism in
inferred type signatures.
Removing this instance required changing the representation of
TcDepVars to use deterministic sets.
This is the last occurence of varSetElemsWellScoped, allowing me to
finally remove it.

Test Plan:
./validate
I will update the expected outputs when commiting, some reordering
of type variables in types is expected.

Reviewers: goldfire, simonpj, austin, bgamari

Reviewed By: simonpj

Subscribers: thomie, simonmar

Differential Revision: https://phabricator.haskell.org/D2135

GHC Trac Issues: #4012

It's possible to get rid of this use site in a local way
and it introduces unneccessary nondeterminism.

Test Plan: ./validate

Reviewers: simonmar, goldfire, austin, bgamari, simonpj

Reviewed By: simonpj

Subscribers: thomie

Differential Revision: https://phabricator.haskell.org/D2122

GHC Trac Issues: #4012

This is from Simon's suggestion:

* `tyCoVarsOfTypesAcc` is a terrible name for a function with a
  perfectly decent type `[Type] -> FV`. Maybe `tyCoFVsOfTypes`?
  Similarly others

* `runFVList` is also terrible, but also has a decent type.
  Maybe just `fvVarList` (and `fvVarSet` for `runFVSet`).

* `someVars` could be `mkFVs :: [Var] -> FV`.

This adds the tyvars of the domain of the substitution into the in-scope
set as well.
What I'm not sure here is if the kinds can have any free vars that
should be in the in-scope set as well.

Test Plan: ./validate

Reviewers: goldfire, austin, bgamari, simonpj

Reviewed By: simonpj

Subscribers: thomie, simonmar

Differential Revision: https://phabricator.haskell.org/D2094

GHC Trac Issues: #11371

This patch finishes off Trac #11450.  Following debate on that ticket,
the patch tightens up the rules for what the instances of an
associated type can look like.  Now they must match the instance
header exactly. Eg

   class C a b where
    type T a x b

With this class decl, if we have an instance decl
  instance C ty1 ty2 where ...
then the type instance must look like
     type T ty1 v ty2 = ...
with exactly
  - 'ty1' for 'a'
  -  'ty2' for 'b', and
  - a variable for 'x'

For example:

  instance C [p] Int
    type T [p] y Int = (p,y,y)

Previously we allowed multiple instance equations and now, in effect,
we don't since they would all overlap.  If you want multiple cases,
use an auxiliary type family.

This is consistent with the treatment of generic-default instances,
and the user manual always said "WARNING: this facility (multiple
instance equations may be withdrawn in the future".

I also improved error messages, and did other minor refactoring.

There should be no change in behaviour here

* Move splitDepVarsOfType(s) from Type to TcType

* Define data type TcType.TcDepVars, document what it means,
  and use it where appropriate, notably in splitDepVarsOfType(s)

* Use it in TcMType.quantifyTyVars and friends

This just defines a useful helper function that was being
duplicated in several places

As pointed out by @simonpj on D2044 we don't need
to compute the free vars of the range of the substitution
as most of them are already carried by the monad.
This should be a tiny performance improvement over the version
from before D2044.

Also removes an extra function that is now unnecessary.

Test Plan: ./validate && ./validate --slow

Reviewers: goldfire, simonpj, austin, bgamari

Reviewed By: simonpj

Subscribers: thomie, simonmar, simonpj

Differential Revision: https://phabricator.haskell.org/D2060

GHC Trac Issues: #11371

We need the free vars of `t2` to satisfy the substitution
invariant. Luckily they are in the in-scope carried around.

Test Plan: ./validate

Reviewers: bgamari, austin, goldfire, simonpj

Reviewed By: simonpj

Subscribers: thomie, simonmar

Differential Revision: https://phabricator.haskell.org/D2044

GHC Trac Issues: #11371

It was Utterly Wrong before.

Note to self: Never, ever take the free vars of an unzonked type.

In particular, this allows correct tracking of specified/invisible
for variables in Haskell98 data constructors and in pattern synonyms.
GADT-syntax constructors are harder, and are left until #11721.

This was all inspired by Simon's comments to my fix for #11512,
which this subsumes.

Test case: ghci/scripts/TypeAppData

[skip ci]  (The test case fails because of an unrelated problem
fixed in the next commit.)

- Optimize zonking * to avoid allocation.
- Try to avoid looking at the free variables of a type in the
  pure unifier. We need look at the variables only in the case
  of a forall.

The performance results updates included in this also include
a regression, but the regression is not due to this patch. When
validating previous patches, the test case failed, but I was
unable to reproduce outside of validation, so I let it go by, thinking
the failure was spurious. Upon closer inspection, the perf number
was right at the line, and the wibble between a valiation environment
and a regular test run was enough to make the difference.

Originally I wanted to only remove substTyWithBindersUnchecked, but
since both of them are unused maybe we don't need them.

Test Plan: ./validate

Reviewers: austin, goldfire, bgamari, simonpj

Reviewed By: simonpj

Subscribers: thomie, simonmar

Differential Revision: https://phabricator.haskell.org/D2025

GHC Trac Issues: #11371