GitLab

Previously, we checked the number of patterns in a data instances
for all data families whose kind did not end in a kind variable.
But, of course, undersaturating instances can happen even without
the kind ending in a kind variable. So I've omitted the arity check.
Data families aren't as particular about their arity as type families
are (because data families can be undersaturated). Still, this change
degrades error messages when instances don't have the right arity;
now, instead of reporting a simple mismatch in the number of patterns,
GHC reports kind errors. The new errors are fully accurate, but perhaps
not as easy to work with. Still, with the new flexibility of allowing
data family instances with varying numbers of patterns, I don't see
a better way.

This commit also improves source fidelity in some error messages,
requiring more changes than really are necessary. But without these
changes, error messages around mismatched associated instance heads
were poor.

test cases: indexed-types/should_compile/T14045,
            indexed-types/should_fail/T14045a

Previously, a data family's kind had to end in `Type`,
and data instances had to list all the type patterns for the
family. However, both of these restrictions were unnecessary:

- A data family's kind can usefully end in a kind variable `k`.
  See examples on #12369.

- A data instance need not list all patterns, much like how a
  GADT-style data declaration need not list all type parameters,
  when a kind signature is in place. This is useful, for example,
  here:

    data family Sing (a :: k)
    data instance Sing :: Bool -> Type where ...

This patch also improved a few error messages, as some error
plumbing had to be moved around.

See new Note [Arity of data families] in FamInstEnv for more
info.

test case: indexed-types/should_compile/T12369

The uo_thing field of TypeEqOrigin is used to track the
"thing" (either term or type) that has the type (kind) stored
in the TypeEqOrigin fields. Previously, this was sometimes a
proper Core Type, which needed zonking and tidying. Now, it
is only HsSyn: much simpler, and the error messages now use
the user-written syntax.

But this aspect of uo_thing didn't cause #13819; it was the
sibling field uo_arity that did. uo_arity stored the number
of arguments of uo_thing, useful when reporting something
like "should have written 2 fewer arguments". We wouldn't want
to say that if the thing didn't have two arguments. However,
in practice, GHC was getting this wrong, and this message
didn't seem all that helpful. Furthermore, the calculation
of the number of arguments is what caused #13819 to fall over.
This patch just removes uo_arity. In my opinion, the change
to error messages is a nudge in the right direction.

Test case: typecheck/should_fail/T13819

Trac #13998 showed that default methods were getting bogus tyvar
binder visiblity info; and that it matters in the code genreated
by the default-method fill-in mechanism

* The actual fix: in TcTyDecls.mkDefaultMethodType, make TyVarBinders
  with the right visibility info by getting TyConBinders from the
  class TyCon.  (Previously we made up visiblity info, but that
  caused #13998.)

* Define TyCon.tyConTyVarBinders :: [TyConBinder] -> [TyVarBinder]
  which can build correct forall binders for
    a) default methods (Trac #13998)
    b) data constructors
  This was originally BuildTyCl.mkDataConUnivTyVarBinders

* Move mkTyVarBinder, mkTyVarBinders from Type to Var

An error message was referring to a type synonym as a datatype.
Annoyingly, learning that the TyCon over which the error message is
operating is actually a type synonym was previously impossible, since
that code only had access to a TcTyCon, which doesn't retain any
information about what sort of TyCon it is.

To rectify this, I created a new TyConFlavour datatype, intended to
capture roughly what sort of TyCon we're dealing with. I then performing
the necessary plumbing to ensure all TcTyCons have a TyConFlavour, and
propagated this information through to the relevant error message.

Test Plan: ./validate

Reviewers: goldfire, austin, bgamari, simonpj

Reviewed By: simonpj

Subscribers: simonpj, rwbarton, thomie

GHC Trac Issues: #13983

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

@goldfire noticed that we don't need to thread through `res_ty`
through to the return type of `rejigConRes`, as it never changes.

Reviewers: goldfire, austin, bgamari

Reviewed By: goldfire

Subscribers: rwbarton, thomie, goldfire

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

Previously, we we only using `tcSplitSigmaTy` when determining if a
function had been applied to too few arguments, so it wouldn't work for
functions with nested `forall`s. Thankfully, this is easily fixed with a
dash of `tcSplitNestedSigmaTys`.

Test Plan: make test TEST=T13311

Reviewers: austin, bgamari, simonpj

Reviewed By: bgamari

Subscribers: goldfire, simonpj, rwbarton, thomie

GHC Trac Issues: #13311

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

Trac #13879 showed that there was a missing zonk in tcLHsKind.

I also renamed it to tcLHsKindSig, for consistency with type signatures
There's a commment to explain why the zonk is needed.

Summary:
See https://ghc.haskell.org/trac/ghc/wiki/ImplementingTreesThatGrow

This commit prepares the ground for a full extensible AST, by replacing the type
parameter for the hsSyn data types with a set of indices into type families,

    data GhcPs -- ^ Index for GHC parser output
    data GhcRn -- ^ Index for GHC renamer output
    data GhcTc -- ^ Index for GHC typechecker output

These are now used instead of `RdrName`, `Name` and `Id`/`TcId`/`Var`

Where the original name type is required in a polymorphic context, this is
accessible via the IdP type family, defined as

    type family IdP p
    type instance IdP GhcPs = RdrName
    type instance IdP GhcRn = Name
    type instance IdP GhcTc = Id

These types are declared in the new 'hsSyn/HsExtension.hs' module.

To gain a better understanding of the extension mechanism, it has been applied
to `HsLit` only, also replacing the `SourceText` fields in them with extension
types.

To preserve extension generality, a type class is introduced to capture the
`SourceText` interface, which must be honoured by all of the extension points
which originally had a `SourceText`.  The class is defined as

    class HasSourceText a where
      -- Provide setters to mimic existing constructors
      noSourceText  :: a
      sourceText    :: String -> a

      setSourceText :: SourceText -> a
      getSourceText :: a -> SourceText

And the constraint is captured in `SourceTextX`, which is a constraint type
listing all the extension points that make use of the class.

Updating Haddock submodule to match.

Test Plan: ./validate

Reviewers: simonpj, shayan-najd, goldfire, austin, bgamari

Subscribers: rwbarton, thomie, mpickering

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

While investigating #12545, I discovered several places in the code
that performed length-checks like so:

```
length ts == 4
```

This is not ideal, since the length of `ts` could be much longer than 4,
and we'd be doing way more work than necessary! There are already a slew
of helper functions in `Util` such as `lengthIs` that are designed to do
this efficiently, so I found every place where they ought to be used and
did just that. I also defined a couple more utility functions for list
length that were common patterns (e.g., `ltLength`).

Test Plan: ./validate

Reviewers: austin, hvr, goldfire, bgamari, simonmar

Reviewed By: bgamari, simonmar

Subscribers: goldfire, rwbarton, thomie

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

Trac #13625 pointed out that in

   data X :: Y where Y :: X

we need 'Y' to be in scope (as APromotionErr) when dealing with
X's kind signature.  Previously we got a crash.

This patch simplifies the code as well as making it work.

This patch

* removes a function TcMType.quantifyTyVars
  that was never called

* renames quantifyZonkedTyVars to quantifyTyVars

Plus a few comments.  No functional change at all

Summary:
RnEnv contains functions which convertn RdrNames into Names.

RnUnbound contains helper functions for reporting and creating
unbound variables.

RnFixity contains code which maintains the fixity environent
whilst renaming.

RnUtils contains the other stuff in RnEnv.

Reviewers: austin, goldfire, bgamari

Subscribers: goldfire, rwbarton, thomie, snowleopard

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

The big change is the introduction of solveSomeEqualities. This
is just like solveEqualities, but it doesn't fail if there are unsolved
equalities when it's all done. Anything unsolved is re-emitted. This
is appropriate if we are not kind-generalizing, so this new form
is used when decideKindGeneralizationPlan says not to.

We initially thought that any use of solveEqualities would be tied
to kind generalization, but this isn't true. For example, we need
to solveEqualities a bunch in the "tc" pass in TcTyClsDecls (which
is really desugaring). These equalities are all surely going to be
soluble (if they weren't the "kc" pass would fail), but we still
need to solve them again. Perhaps if the "kc" pass produced type-
checked output that is then desugared, solveEqualities really would
be tied only to kind generalization.

Updates haddock submodule.

Test Plan: ./validate, typecheck/should_compile/T13337

Reviewers: simonpj, bgamari, austin

Reviewed By: simonpj

Subscribers: RyanGlScott, rwbarton, thomie

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

Summary:
Previously, abstract classes looked very much like normal
classes, except that they happened to have no methods,
superclasses or ATs, and they came from boot files.  This
patch gives abstract classes a proper representation in
Class and IfaceDecl, by moving the things which are never
defined for abstract classes into ClassBody/IfaceClassBody.

Because Class is abstract, this change had ~no disruption
to any of the code in GHC; if you ask about the methods of
an abstract class, we'll just give you an empty list.

This also fixes a bug where abstract type classes were incorrectly
treated as representationally injective (they're not!)

Fixes #13347, and a TODO in the code.
Signed-off-by: Edward Z. Yang <ezyang@cs.stanford.edu>

Test Plan: validate

Reviewers: simonpj, bgamari, austin

Subscribers: goldfire, thomie

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

Summary:
This commit implements the plan in #13140:

* Today, roles in signature files default to representational. Let's change the
  default to nominal, as this is the most flexible implementation side. If a
  client of the signature needs to coerce with a type, the signature can be
  adjusted to have more stringent requirements.

* If a parameter is declared as nominal in a signature, it can be implemented
  by a data type which is actually representational.

* When merging abstract data declarations, we take the smallest role for every
  parameter. The roles are considered fix once we specify the structure of an
  ADT.

* Critically, abstract types are NOT injective, so we aren't allowed to
  make inferences like "if T a ~R T b, then a ~N b" based on the nominal
  role of a parameter in an abstract type (this would be unsound if the
  parameter ended up being phantom.)  This restriction is similar to the
  restriction we have on newtypes.
Signed-off-by: Edward Z. Yang <ezyang@cs.stanford.edu>

Test Plan: validate

Reviewers: simonpj, bgamari, austin, goldfire

Subscribers: goldfire, thomie

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

Summary:
Fixes #13335.
Signed-off-by: Edward Z. Yang <ezyang@cs.stanford.edu>

Test Plan: validate

Reviewers: goldfire, austin, simonpj, bgamari

Subscribers: thomie

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

Previously TcTyCons were used only for knot-tying, but now they
are also used after an error, to add a benign TyCon to the envt
so we can carry on; see TyCon.makeRecoveryTyCon.  But since it
is used in this way, subsequent declarations may see a TcTyCon
(e.g. during injectivity checks) and should not have a heart attack
as a result.

See Note [TcTyCon] in TyCon.

This fixes Trac #13271

Before, GHC was extremely permissive about the form a default type
signature could take on in a class declaration. Notably, it would accept
garbage like this:

  class Monad m => MonadSupply m where
    fresh :: m Integer
    default fresh :: MonadTrans t => t m Integer
    fresh = lift fresh

And then give an extremely confusing error message when you actually
tried to declare an empty instance of MonadSupply. We now do extra
validity checking of default type signatures to ensure that they align
with their non-default type signature counterparts. That is, a default
type signature is allowed to differ from the non-default one only in its
context - they must otherwise be alpha-equivalent.

Fixes #12918.

Test Plan: ./validate

Reviewers: goldfire, simonpj, austin, bgamari

Reviewed By: bgamari

Subscribers: mpickering, dfeuer, thomie

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

GHC Trac Issues: #12918

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.

Summary:
With hs-boot files, some type families may be defined in the
module we are typechecking.  In this case, we are not allowed
to poke these families until after we typecheck our local
declarations.  So we first check everything involving non-recursive
families, and then check the recursive families as we finish
kind-checking them.
Signed-off-by: Edward Z. Yang <ezyang@cs.stanford.edu>

Test Plan: validate

Reviewers: goldfire, austin, simonpj, bgamari

Subscribers: thomie

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

GHC Trac Issues: #11062

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:
Add prettyprinter tests, which take a file, parse it, pretty print it,
re-parse the pretty printed version and then compare the original and
new ASTs (ignoring locations)

Updates haddock submodule to match the AST changes.

There are three issues outstanding

1. Extra parens around a context are not reproduced. This will require an
   AST change and will be done in a separate patch.

2. Currently if an `HsTickPragma` is found, this is not pretty-printed,
   to prevent noise in the output.

   I am not sure what the desired behaviour in this case is, so have left
   it as before. Test Ppr047 is marked as expected fail for this.

3. Apart from in a context, the ParsedSource AST keeps all the parens from
   the original source.  Something is happening in the renamer to remove the
   parens around visible type application, causing T12530 to fail, as the
   dumped splice decl is after the renamer.

   This needs to be fixed by keeping the parens, but I do not know where they
   are being removed.  I have amended the test to pass, by removing the parens
   in the expected output.

Test Plan: ./validate

Reviewers: goldfire, mpickering, simonpj, bgamari, austin

Reviewed By: simonpj, bgamari

Subscribers: simonpj, goldfire, thomie, mpickering

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

GHC Trac Issues: #3384

I found that some TcTyVars were lurking in a PatSyn, because
tc_patsyn_finish was using the TcType -> TcType zonker rather
than the TcType -> Type zonker.  Eeek.

I fixing this I also tided up function naming a bit (still not
terrific), and removed the unused TcTyBinder type entirely.

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

Pass in a Bool rather than return a funcion!

No change in behaviour.

* I found a bug in 'generalize' in TcTyClsDecls.kcTyClGroup, where
  the kind variables weren't being turned into proper TyVars, so
  we got (skolem) TcTyVars in TyCons, which shouldn't happen.  Fix
  was easy.

* Similarly TcHsType.kindGeneralizeType wasn't turning the forall'd
  TcTyVars into TyVars.  To achieve this I defined TcHsTyn.zonkSigType.

* All this allowed me to remove awkward and ill-explained bit of
  footwork on DFunIds in Inst.newClsInst

This is just refactoring, but it does make the printout from
-ddump-deriv make a bit more sense by not grautuitiously cloning
type variables.  In the display I was seeing

   instance C [a_df4] where
      f x = ...a_dx5...

where actually the d_df4 and a_dx5 were the same.

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.

Summary:
In the old implementation of hsig files, we directly
reused the implementation of abstract data types from
hs-boot files.  However, this was WRONG.  Consider the
following program (an abridged version of bkpfail24):

    {-# LANGUAGE GADTs #-}
    unit p where
        signature H1 where
            data T
        signature H2 where
            data T
        module M where
            import qualified H1
            import qualified H2

            f :: H1.T ~ H2.T => a -> b
            f x = x

Prior to this patch, M was accepted, because the type
inference engine concluded that H1.T ~ H2.T does not
hold (indeed, *presently*, it does not).  However, if
we subsequently instantiate p with the same module for
H1 and H2, H1.T ~ H2.T does hold!  Unsound.

The key is that abstract types from signatures need to
be treated like *skolem variables*, since you can interpret
a Backpack unit as a record which is universally quantified
over all of its abstract types, as such (with some fake
syntax for structural records):

    p :: forall t1 t2. { f :: t1 ~ t2 => a -> b }
    p = { f = \x -> x } -- ill-typed

Clearly t1 ~ t2 is not solvable inside p, and also clearly
it could be true at some point in the future, so we better
not treat the lambda expression after f as inaccessible.

The fix seems to be simple: do NOT eagerly fail when trying
to simplify the given constraints.  Instead, treat H1.T ~ H2.T
as an irreducible constraint (rather than an insoluble
one); this causes GHC to treat f as accessible--now we will
typecheck the rest of the function (and correctly fail).
Per the OutsideIn(X) paper, it's always sound to fail less
when simplifying givens.

We do NOT apply this fix to hs-boot files, where abstract
data is also guaranteed to be nominally distinct (since
it can't be implemented via a reexport or a type synonym.)
This is a somewhat unnatural state of affairs (there's
no way to really interpret this in Haskell land) but
no reason to change behavior.

I deleted "representationally distinct abstract data",
which is never used anywhere in GHC.

In the process of constructing this fix, I also realized
our implementation of type synonym matching against abstract
data was not sufficiently restrictive.  In order for
a type synonym T to be well-formed type, it must be a
nullary synonym (i.e., type T :: * -> *, not type T a = ...).
Furthermore, since we use abstract data when defining
instances, they must not have any type family applications.

More details in #12680.  This probably deserves some sort
of short paper report.
Signed-off-by: Edward Z. Yang <ezyang@cs.stanford.edu>

Test Plan: validate

Reviewers: goldfire, simonpj, austin, bgamari

Subscribers: thomie

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

Newtypes cannot (currently) have an unboxed argument type.
But Trac #12729 showed that this was only being checked for
newtypes in H98 syntax; in GADT snytax they were let through.

This patch moves the test to checkValidDataCon, where it properly
belongs.

In tcFamTyPats we were zonking from the TcType world to the
Type world, ready to build the results into a CoAxiom (which
should have no TcType stuff.  But the 'thing_inside' for
tcFamTyPats also must be zonked, and that zonking must have
the ZonkEnv from the binders zonked tcFamTyPats.

Ugh.  This caused an assertion failure (with DEBUG on) in
RaeBlobPost and TypeLevelVec, both in tests/dependent, as
shown in Trac #12682.  Why it hasn't shown up before now
is obscure to me.

So I moved the zonking stuff out of tcFamTyPats to its
three call sites, where we can do it all together. Very
slightly longer, but much more robust.

Fixes Trac #7497 and #12151.   In some earlier upheaval I introduced
a bug in the ambiguity check for genreric-default method.

This patch fixes it.  But in fixing it I realised that the
sourc-location of any such error message was bogus, so I fixed
that too, which involved a slightly wider change; see the
comments with TcMethInfo.