Improve printing of pattern synonym types
ClosedPublic

Authored by mpickering on Feb 9 2016, 3:30 AM.

Details

Summary

Add the function pprPatSynType :: PatSyn -> SDoc for printing pattern
synonym types, and remove the ambiguous patSynType function. Also,
the types in a PatSyn are now tidy.

Fixes: Trac #11213.

Diff Detail

Repository
rGHC Glasgow Haskell Compiler
Lint
Automatic diff as part of commit; lint not applicable.
Unit
Automatic diff as part of commit; unit tests not applicable.
There are a very large number of changes, so older changes are hidden. Show Older Changes
mpickering edited edge metadata.Feb 9 2016, 9:10 AM

I think this is a lot more complicated that it needs to be! Both places where pprPatSynType is called, it's argument has just been constructed by using patSynType. In other words, why not write a function pprPatSynType :: PatSyn -> SDoc which directly prints the type rather than this rather hairy indirection counting the number of contexts in prov/req theta?

This revision now requires changes to proceed.Feb 9 2016, 9:10 AM

Thanks for looking at the patch.

You are right that now the only places where pprPatSynType is used an instance of PatSyn is available. However, I wasn't sure if this would always be the case. I've not yet identified all places where pprPatSynType should be called. I forgot to mention this. I'll try to find all those places (an instance of PatSyn is not created until tc_patsyn_finish is called).

Another reason why I chose to use a single Type instance to represent the type of a pattern synonym, is that this makes it easy to tidy the type. We can handle both sigma types and pattern synonym types in the same way (see get_msg in warnMissingSigs in rename/RnNames.hs).

simonpj resigned from this revision.Feb 9 2016, 3:22 PM
simonpj removed a reviewer: simonpj.

I think the types in a PatSyn should be already tidy. I do suggest starting from PatSyn rather than decomposing a Type.

compiler/rename/RnNames.hs
1589

To me this seems very odd.

We start with a lovely, structured PatSyn, p.

We extract from it a triple (type, n_ex, n_prov)

Then we finally pass that triple to pprPatSynType.

It unpacks the triple and passes it to the (badly named) ppr_pat_syn_type. (It's badly named because it is also used for ordinary types, via

ppr_sigma_type fa_choice ty = ppr_patsyn_type fa_choice ty 0 0

.)

Finally it prints the type.

Why go to all this trouble? Why not just write a pretty-printer with type

pprPatSynType :: PatSyn -> SDoc

which will be easy to write? (Indeed much of the work is already done by pprPatSynSig, which is badly placed in HsBinds and is only used from IfaceSyn.)

I feel I must be missing something but it all seems over-complicated .

1612

I'm intrigued by the reduction in code size here.... great.... but where has it gone?!!

compiler/types/TyCoRep.hs
2315 ↗(On Diff #6592)

Is the need for ForAllChoice driven by pattern synonyms, or by something orthogonal?

rdragon updated this revision to Diff 6611.Feb 10 2016, 1:34 PM
rdragon edited edge metadata.

Use pprPatSynType in pprSigSkolInfo

Also, rename ppr_patsyn_type to ppr_patsyn_like_type.

I've added a call to pprPatSynType in pprSigSkolInfo. Now errors like

module Mod1 where
pattern Pat :: Show a => Ord a => a -> Maybe a
pattern Pat x <- Just x

Mod1.hs:5:23: error:
    * Could not deduce (Ord a) arising from a pattern
      from the context: Show a
        bound by the type signature for pattern synonym `Pat':
                   a -> Maybe a
        at Mod1.hs:5:9-11
        ...

are printed with the correct pattern types:

Mod1.hs:5:23: error:
    * Could not deduce (Ord a) arising from a pattern
      from the context: Show a
        bound by the type signature for pattern synonym `Pat':
                   forall a1. Show a1 => Ord a1 => a1 -> Maybe a1
        at Mod1.hs:5:9-11
        ...

In pprSigSkolInfo an instance of PatSyn is not yet available. Therefore, I think a function PatSyn -> SDoc does not suffice. Please tell me if I'm wrong. I do see that we now take an indirect route. However, the decomposition of a Type instance needs to be done either way, as it is needed for printing sigma types.

Maybe a more understandable solution (but which I think will require more code) is for example to create the following (exported) functions:

TyCoRep.hs:
ppr_patsyn_type :: [TyVar] -> ThetaType -> [TyVar] -> ThetaType -> [Type] -> Type -> SDoc
ppr_user_patsyn_type :: [TyVar] -> ThetaType -> [TyVar] -> ThetaType -> [Type] -> Type -> SDoc

PatSyn.hs:
pprPatSynType :: PatSyn -> SDoc
pprUserPatSynType :: PatSyn -> SDoc

TcRnTypes.hs:
pprPatSynType :: TcPatSynInfo -> SDoc
pprUserPatSynType :: TcPatSynInfo -> SDoc

Here we use the TyCoRep.hs functions to define the other functions.

We could also create a new data type PatSynInfo that is identical to TcPatSynInfo (and define type TcPatSynInfo = PatSynInfo). This allows us to create instead functions like patSynInfo :: PatSyn -> PatSynInfo and pprPatSynType :: PatSynInfo -> SDoc.

compiler/rename/RnNames.hs
1612

All the functionality is still there, but it is now inside warnMissingSigs. The top-level functions weren't exported or used anywhere else. Is this not okay?

compiler/types/TyCoRep.hs
2315 ↗(On Diff #6592)

There is no need for ForAllChoice. I thought it made the code more clear than using a boolean. Now you can see right away which functions print the foralls unconditionally and which do not.

rdragon updated this revision to Diff 6617.Feb 11 2016, 5:57 AM
rdragon edited edge metadata.

Fix pprIfaceDecl for IfacePatSyn arguments

Now the pattern signature from Trac #11524 correctly prints as

*Mod1> :info PApp
pattern PApp :: forall k (fun :: k). forall k1 (a :: k1
                                                     -> k) (b :: k1). fun ~ a b => AType a
                                                                                   -> AType b
                                                                                   -> AType fun
        -- Defined at Mod1.hs:9:1

Is it allowed to use sep instead of hsep to make this print more pretty?

Oh, I guess GHC requires an explicit empty context between the two foralls to differentiate between the universals and existentials. I'll fix the printing.

I'll also repair the loop created by the import import TcMType ( checkingExpType ).

rdragon updated this revision to Diff 6627.Feb 12 2016, 7:30 AM
rdragon edited edge metadata.

Change printing of patsyn type and fix build

rdragon updated this revision to Diff 6646.Feb 15 2016, 3:39 AM
rdragon edited edge metadata.

Undo the change to pprSigSkolInfo

This was not the right solution for printing the correct pattern synonym signature from a SigSkol PatSynCtxt ExpType. (It looks like the ExpType should at least not contain the forall univ_tvs part of the type, but if you do add the req => forall ex_tvs. prov => part, then in some error messages the full signature is not shown (only in one case the forall univ_tvs is added again).)

rdragon updated this revision to Diff 6664.Feb 16 2016, 8:56 AM
rdragon edited edge metadata.

Add test T11524a

This one tests the output of the :info command on pattern synonyms.

(It is possible to split this revision in one that accepts test T11213 and one that accepts test T11524a. Just ask me.)

@rdragon: what is the status here? Are you still working on it, or waiting for review?

I still think this packing/unpacking is quite dodgy.

What do you mean by this?

However, the decomposition of a Type instance needs to be done either way, as it is needed for printing sigma types.

Did sigma types not print fine before? What problem has it solved.

I agree that SigSkolInfo is a bit of a problem but I don't know if the additional complexity is worth it for this one case. Maybe just not printing a type here would be ok? I haven't looked in detail yet.

What do you mean by this?

However, the decomposition of a Type instance needs to be done either way, as it is needed for printing sigma types.

Did sigma types not print fine before? What problem has it solved.

What I mean is that before the patch, ppr_sigma_type contained code to unpack a type (split it into the quantified variables, the constraints, and the rest). So the unpacking was already needed, now we only need to unpack it a bit further (split the variables into univ / ex, and split the constraints into req / prov).

Your suggestion of not printing a pattern synonym type when a PatSyn instance is not yet available might be a good idea. Here are two examples.

Example 1:

pattern Pat :: Eq a => Show a => a -> Maybe a
pattern Pat x <- Just x

Mod1.hs:4:23: error:
    * Could not deduce (Show a)
        arising from the "provided" constraints claimed by
          the signature of `Pat'
      from the context: Eq a
        bound by the type signature for pattern synonym `Pat':
                   Eq a => Show a => a -> Maybe a
        at Mod1.hs:4:9-11
    * In the declaration for pattern synonym `Pat'

Here we could perhaps remove the whole "from the context ... at Mod1.hs:4:9-11" part, as I would think that it doesn't make much sense to define a pattern synonym with a "provided" constraint that is deducible from the "required" context (all constraints that are deducible from the "required" context will already be available at a usage site of the pattern synonym). So then a better error message would be:

Mod1.hs:4:23: error:
    * No instance for (Show a)
        arising from the "provided" constraints claimed by
          the signature of `Pat'
      In other words, a successful match on the pattern
        Just x
      does not provide the constraint (Show a)
    * In the declaration for pattern synonym `Pat'

Example 2:

data T where MkT :: a -> T

pattern Pat :: a -> T
pattern Pat x <- MkT x

f :: T -> Int
f (Pat x) = x

Mod1.hs:10:13: error:
    * Couldn't match expected type `Int' with actual type `a'
      `a' is a rigid type variable bound by
        a pattern with pattern synonym: Pat :: () => forall a. a -> T,
        in an equation for `f'
        at Mod1.hs:10:4
    * In the expression: x
      In an equation for `f': f (Pat x) = x
    * Relevant bindings include x :: a (bound at Mod1.hs:10:8)

I guess here it is not a big problem to just say "a pattern with pattern synonym Pat".

Mod1.hs:4:23: error:
    * No instance for (Show a)
        arising from the "provided" constraints claimed by
          the signature of `Pat'
      In other words, a successful match on the pattern
        Just x
      does not provide the constraint (Show a)
    * In the declaration for pattern synonym `Pat'

I think this is good. With this chance, everything will be much simpler.

mpickering requested changes to this revision.Feb 27 2016, 5:03 AM
mpickering edited edge metadata.
This revision now requires changes to proceed.Feb 27 2016, 5:03 AM
rdragon updated this revision to Diff 6830.Mar 5 2016, 10:27 AM
rdragon edited edge metadata.
rdragon added a subscriber: simonpj.

Now with PatSyn -> SDoc function

As suggested by @mpickering and @simonpj we create a function pprPatSynType :: PatSyn -> SDoc.

Also, part of this patch has been removed and can now be found in D1958 and D1967. Together, these patches should fix most (all?) problems associated with printing pattern synonym types.

rdragon updated this object.Mar 5 2016, 10:29 AM
rdragon edited edge metadata.

I think the types in a PatSyn should be already tidy.

It looks like tidying is required for the types in a PatSyn. Otherwise, test T11213 fails for the patterns Purep and Pure. Here is the difference for the pattern Pure:

-Pure :: forall a. (Num a, Eq a) => forall a1. a -> a1 -> ([a], Ex)
+Pure :: forall a. (Num a, Eq a) => forall a. a -> a -> ([a], Ex)
compiler/basicTypes/PatSyn.hs
440

I'm not entirely sure if emptyTidyEnv is the right choice. I would think so since pattern synonym declarations are only valid at top level. However, if emptyTidyEnv can be used at top level, then I do not understand why warnMissingSignatures uses tcInitTidyEnv instead of emptyTidyEnv (rename\RnNames.hs, line 1605).

Two more comments, this looks much cleaner than before. Thanks for sticking with it!

compiler/basicTypes/PatSyn.hs
440

Well, GHC can also warn about missing local sigs with -Wmissing-local-sigs. Does that answer your question?

testsuite/tests/patsyn/should_compile/T11213.stderr
2

Is this sterr right? I thought that the in -Wall part of the message got turned off by default. How recently have you rebased?

rdragon added inline comments.Mar 7 2016, 3:54 AM
compiler/basicTypes/PatSyn.hs
440

If GHC uses warnMissingSignatures in RnNames.hs to print these missing local signatures then this would indeed answer my question. However, there is another warnMissingSignatures in TcBinds.hs and that is the one used for printing missing local signatures.

testsuite/tests/patsyn/should_compile/T11213.stderr
2

Test T11053 also sets -fwarn-missing-pattern-synonym-signatures and has (in -Wall) in its stderr (testsuite/tests/patsyn/should_fail/T11053.stderr), so I guess this stderr is right.

I've suggested a couple of irmprovements

compiler/basicTypes/PatSyn.hs
431

An attractive alternative would be to tidy the (inferred) type of a pattern synonym *at construction* (in `tc_patsyn_finish" rather than every time we print it.

Not only does that seem neater, but it also means that the type variable names used when we instantiate it would line up with the ones in its type signature.

compiler/rename/RnNames.hs
1587

If it were me, I'd do two forMs, one for the Id binders and one for the patsyn binders. As it stands you need to build this list of pairs with a monadic second component that takes a bit of of unravelling.

Not a big deal, but I think you'd find it was simpler. Also you could wrap the patsyn one with when warn_pat_syns which is very simple and direct compared with making patsyns be empty if warn_pat_syns is false.

bollmann added a subscriber: bollmann.EditedMar 8 2016, 4:23 AM

@rdragon, @mpickering @simonpj @goldfire: I'm currently adding pattern synonym support to template haskell (see Trac #8761 and D1940 for details). For the reification of pattern synonyms I need a function just like what we had before, namely: patSynType :: PatSyn -> Type. However, I need this function patSynType :: PatSyn -> Type to behave exactly as given in your testcases T11213.stderr (i.e., it may not simply "forget" an empty required constraint context, as it does now). A function pprPatSynType :: PatSyn -> SDoc wouldn't work as well, since the existing reification infrastructure in TcSplice works based on Types rather than SDocs.

Do you think we can therefore have a corrected version of patSynType :: PatSyn -> Type as well?

Btw: Your tests seem very complete wrt the possible typings of a pattern synonym. May I reuse them to test reification of pattern synonyms? :-)

testsuite/tests/patsyn/should_compile/T11213.stderr
22

shouldn't this case have the type signature Purp :: forall a t. (Num a, Eq a, Show t) => a -> t -> ([a], UnivProv t), since we're only dealing with universals here?

As far as I know, it is not possible to create a 'correct' function patSynType :: PatSyn -> Type. This has to do with the formulation of the type Type. In particular, an explicit empty context cannot be represented in Type, see also Note [Patterns synonyms and the data type Type] in D1967.

The patSynType :: PatSyn -> Type that was here before returned an ambiguous value. Only with additional information (the number of existential type variables and the size of the "provided" context) it was possible to reconstruct the full type of the pattern synonym from this value (this full type cannot be represented by a value of type Type).

Btw: Your tests seem very complete wrt the possible typings of a pattern synonym. May I reuse them to test reification of pattern synonyms? :-)

Yes, ofcourse!

testsuite/tests/patsyn/should_compile/T11213.stderr
22

We are indeed only dealing with universally quantified type variables here. However, these variables are allowed to occur in the "provided" context, and moreover, it is possible to have a "provided" context without any existentially quantified type variables. This is an example with such a context.

bollmann added a comment.EditedMar 8 2016, 6:56 AM

actually, the more I think about reification of pattern synonyms in Template Haskell, the more I come to the conclusion that a function of patSynType :: PatSyn -> Type won't solve my problems because Type does not contain enough structure to also denote when there is an empty constraint set somewhere in the type (e.g., for explicitly expressing that in pattern synonyms the required constraint set is empty rather than omitting it).

Therefore, I think I'll just build up reification from its raw parts provided by patSynSig.

EDIT: @rdragon, sorry, I didn't see your comment before. Thanks for the confirmation about patSynType. I won't be needing it in this case either, so go ahead with what you were doing. Sorry for all the noise!

And thanks for being able to reuse your tests! :-)

@rdragon Do you want me to finish this ticket off?

@rdragon Do you want me to finish this ticket off?

Thanks, but that won't be necessary. I'll update the ticket today.

rdragon updated this revision to Diff 6937.Mar 15 2016, 10:07 AM

Tidy in tc_patsyn_finish and refactor warnMissingSignatures

I've suggested a couple of irmprovements

Thanks for the suggestions. Both improvements are now included.

simonpj accepted this revision.Mar 16 2016, 10:31 AM
simonpj added a reviewer: simonpj.

Much nicer. One further suggestion

compiler/typecheck/TcPatSyn.hs
423

I'm not sure you need all these has_sig tests. If there is a signature,tidying will be a no-op. So you can tidy regardless

rdragon updated this revision to Diff 6945.Mar 16 2016, 2:42 PM
rdragon edited edge metadata.

Remove has_sig checks

rdragon updated this object.Mar 16 2016, 2:44 PM
rdragon edited edge metadata.
mpickering accepted this revision.Mar 16 2016, 6:25 PM
mpickering edited edge metadata.

@rdragon Thanks for sticking with this!

This revision is now accepted and ready to land.Mar 16 2016, 6:25 PM
bgamari requested changes to this revision.Mar 20 2016, 12:30 PM
bgamari edited edge metadata.

Do you have a patch updating haddock's Convert module for the loss of patSynType?

This revision now requires changes to proceed.Mar 20 2016, 12:30 PM

Do you have a patch updating haddock's Convert module for the loss of patSynType?

Oops, I hadn't checked the other repositories for uses of patSynType. I've created a patch for Haddock, see D2048.

mpickering commandeered this revision.Apr 2 2016, 4:42 PM
mpickering edited reviewers, added: rdragon; removed: mpickering.

Thanks @rdragon.

I committed the patch with the relevant haddock update. https://github.com/ghc/ghc/commit/72bd7f7be7809076f321a6fca90024e3e1bde3cc

mpickering abandoned this revision.Apr 2 2016, 4:43 PM
This revision was automatically updated to reflect the committed changes.