#8776 closed bug (fixed)

Displaying pattern synonym for a GADT

Reported by: monoidal Owned by: cactus
Priority: normal Milestone:
Component: Compiler Version: 7.7
Keywords: Cc: cactus
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Revisions:



{-# LANGUAGE PatternSynonyms, GADTs #-}
data A x y where
  B :: A x x

pattern P = B

and in GHCi we see

λ> :i P
pattern (t ~ t) => P :: A t t1 	-- Defined at X.hs:5:9

It should be (t ~ t1). Just a problem with displaying, the pattern works correctly.

Change History (17)

comment:1 Changed 16 months ago by monoidal

We don't even need full GADTs:

data A x y = (Num x, Eq y) => B

pattern P = B

comment:2 Changed 15 months ago by cactus

Using -dppr-debug shows that the two type variables are distinct and correct:

(base:GHC.Num.Num{tc 2b} t{tv aQa} [sk],
 ghc-prim:GHC.Classes.Eq{tc 23} t{tv aQb} [sk]) =>
main:Main.P{d rs2} :: main:Main.A{tc rpC} t{tv aQa} [sk] t1{tv aQb} [sk]

comment:3 Changed 15 months ago by cactus

When you do a :t P in GHCi, it runs PprTyThings.pprPatSyn, which uses TypeRep.pprTheta to print both contexts:

pprPatSyn :: PatSyn -> SDoc
pprPatSyn patSyn
  = pprPatSynSig ident is_bidir args (pprTypeForUser rhs_ty) prov req
    ident = patSynId patSyn
    is_bidir = isJust $ patSynWrapper patSyn

    args = fmap pprParendType (patSynTyDetails patSyn)
    prov = pprThetaOpt prov_theta
    req = pprThetaOpt req_theta

    pprThetaOpt [] = Nothing
    pprThetaOpt theta = Just $ pprTheta theta

    (_univ_tvs, _ex_tvs, (prov_theta, req_theta)) = patSynSig patSyn
    rhs_ty = patSynType patSyn

So it seems to me that the problem is pprTheta pretty-printing the context constraint-by-constraint, without any regard to possible name clashes between mentioned type variables.

comment:4 Changed 15 months ago by cactus

I am off for next week in an hour and I don't really know my way in the world of OutputBndr. If anyone can help based on the diagnosis above, please jump in in time for GHC 7.8.

comment:5 Changed 15 months ago by simonpj

Gergo writes (to ghc-devs):The problem is that the two type variables occurring in the provided context both have "t" as their user-visible name; even though the second one is projected as "t1" in the tau type on the right-hand side.

The code to generate this output is in HsBinds.ppr_sig, using pprPatSynSig which just adds the "pattern" keyword and the separating "=>" symbols etc:

ppr_sig (PatSynSig name arg_tys ty prov req)
   = pprPatSynSig (unLoc name) False args (ppr ty) (pprCtx prov) (pprCtx req)
     args = fmap ppr arg_tys

     pprCtx lctx = case unLoc lctx of
         [] -> Nothing
         ctx -> Just (pprHsContextNoArrow ctx)

My guess is that the problem is pprHsContextNoArrow projects individual constraints one-by-one and so doesn't notice the name clash on 't' between the two constraints in the example; whereas 'ppr ty' walks the whole right-hand tau type and thus has the opportunity to maintain a set of type variable names used.

My question is, where is that logic, and how can I use that in this instance? My hope is to be shown a design where I can run 'ppr ty', 'pprCtx prov' and 'pprCtx req' in the same "naming environment" (I hope such a thing exists) so that they use a consistent naming scheme. This looks like a problem that must have popped up at a lot of places in GHC already and must have an idiomatic solution.

comment:6 Changed 15 months ago by simonpj

Yes, this does pop up, and there is only half of an idiomatic solution.

  • When pretty-printing (a type, say), the idiomatic solution is not to "rename type variables on the fly", but rather to "tidy" the type (which gives each variable a distinct print-name), and then pretty-print it (without renaming). Separate the two concerns. Functions like tidyType do this.
  • Alas, for type constructors, TyCon, tidying does not work well, because a TyCon includes DataCons which include Types, which mention TyCons. And tidying can't tidy a mutually recursive data structure graph, only trees.
  • One alternative would be to ensure that TyCons get type variables with distinct print-names. That's ok for type variables but less easy for kind variables. Processing data type declarations is already so complicated that I don't think it's sensible to add the extra requirement that it generates only "pretty" types and kinds.
  • One place the non-pretty names can show up is in GHCi. But another is in interface files. Look at MkIface.tyThingToIfaceDecl which converts a TyThing (i.e. TyCon, Class etc) to an IfaceDecl. And it does tidying as part of that conversion. Why? Because interface files contains fast-strings, not uniques, so the names must at least be distinct. (You can see this happening for pattern synonyms in patSynToIfaceDecl.
  • SO MY PLAN is that the :info stuff in GHCi should work in two stages:
    • Use tyThingToIfaceDecl to convert the TyThing to an IfaceDecl
    • Pretty print that.

Nothing very hard. It requires quite a bit of re-working in PprTyThing, but I think fairly routine.

comment:7 Changed 15 months ago by cactus

  • Owner set to cactus

OK I have pushed a prototype implementation of that to the T8776 branch. It changes ppr_ty_thing to go via the IfaceDecl, but only for PatSynCon, since tyThingToIfaceDecl doesn't work for RealDataCons. If you think that makes sense, I can clean it up somewhat (by removing remnants of the old way to print PatSynCon TyThings) and merge it to master.

comment:8 Changed 15 months ago by simonpj


Yes that looks right to me, thank you. Do remove the remnants and merge. It's nice that it eliminates some duplication.

Maybe add the comments above as a Note to explain the strategy.

For RealDataCon, you can generate an IfaceId decl, because that will print just the way that pprDataConSig worked.

If you felt brave you could try converting some of the other cases. AnId is simple, and ACoAxiom is probably simple too.


Last edited 15 months ago by simonpj (previous) (diff)

comment:9 Changed 15 months ago by cactus

  • Status changed from new to merge

OK I've done all but ATyCon. It's merged into master and should be ready to be picked up into ghc-7.8.

comment:10 Changed 15 months ago by simonpj

Did you come across any particular obstacles with TyCon?

comment:11 Changed 15 months ago by cactus

I may have to back out on AnId since it always prints explicit foralls, which could confuse newbies. Let's see if it's possible to know from an IfaceId if it was originally defined with explicit foralls.

comment:12 Changed 15 months ago by simonpj

Gergo, it's all fine, but just needs a bit more refactoring:

  • PprTyThing.pprTypeForUser consults a flag -fprint-explicit-foralls to see whether to print the foralls.
  • So we should call pprTypeForUser when printing types in IfaceDecls (since we are now converting TyThings to IfaceDecls before printing.
  • That means moving pprTypeForUser to IfaceSyn; or perhaps even all the way into TypeRep with the other type-printing machinery.
  • Currently pprTypeForUser also tidies the type. That is not necessary (and therefore confusing) when printing IfaceDecls since they are already tidy. It is only necessary for the calls in ghc/InteractiveUI where we print un-tidy types and kinds. So we could do with a variant (even locally in InteractiveUI that tides the type and then calls pprTypeForUser, where the latter no longer does tidying).

Does that make sense?

I'm unclear how much, if any, of this we should try to get into 7.8. I don't want to destablise the release. Pattern synonyms are new, so if :info doesn't work very well in 7.8 that's probably acceptable.


Last edited 15 months ago by simonpj (previous) (diff)

comment:13 Changed 15 months ago by cactus

I've wasted too much time trying to get it to work... While the general idea is sound, there's one tiny problem that unfortunately breaks the whole thing: IfaceType's ppr_ty has no way of splitting an IfaceType into a theta and a tau, because isIfacePredTy is stubbed out:

isIfacePredTy :: IfaceType -> Bool
isIfacePredTy _  = False
-- FIXME: fix this to print iface pred tys correctly
-- isIfacePredTy ty = isConstraintKind (ifaceTypeKind ty)

and there's no obvious way to implement ifaceTypeKind either...

comment:14 Changed 15 months ago by Dr. ERDI Gergo <gergo@…>

In 52003696ff7a2bbf86fbfccfe29b9f146a1ea549/ghc:

Reinstate pretty-printing of AnIds via pprId (#8776)

comment:15 Changed 15 months ago by Dr. ERDI Gergo <gergo@…>

In de32a95ef21970c2db959509861b4f59d1dcbb82/ghc:

Add test case for #8776

comment:16 Changed 15 months ago by cactus


I've reverted the part of the change that tunneled AnIds via the IfaceDecl path. We should have a discussion on the eventual Correct(tm) implementation, but for now, this passes all the existing GHCi tests and also fixes the pattern synonym issue at hand.

comment:17 Changed 14 months ago by thoughtpolice

  • Resolution set to fixed
  • Status changed from merge to closed

This is all merged into 7.8.

Note: See TracTickets for help on using tickets.