[GHC] #8776: Displaying pattern synonym for a GADT
#8776: Displaying pattern synonym for a GADT ------------------------------------+------------------------------------- Reporter: monoidal | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Keywords: | Operating System: Unknown/Multiple Architecture: Unknown/Multiple | Type of failure: None/Unknown Difficulty: Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | ------------------------------------+------------------------------------- Define {{{ {-# 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8776 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8776: Displaying pattern synonym for a GADT -------------------------------------+------------------------------------ Reporter: monoidal | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by monoidal): We don't even need full GADTs: {{{ data A x y = (Num x, Eq y) => B pattern P = B }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8776#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8776: Displaying pattern synonym for a GADT -------------------------------------+------------------------------------ Reporter: monoidal | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by cactus): Using `-dppr-debug` shows that the two type variables are distinct and correct: {{{ pattern (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] }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8776#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8776: Displaying pattern synonym for a GADT -------------------------------------+------------------------------------ Reporter: monoidal | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (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 where 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8776#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8776: Displaying pattern synonym for a GADT -------------------------------------+------------------------------------ Reporter: monoidal | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8776#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8776: Displaying pattern synonym for a GADT -------------------------------------+------------------------------------ Reporter: monoidal | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (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) where 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8776#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8776: Displaying pattern synonym for a GADT -------------------------------------+------------------------------------ Reporter: monoidal | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (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 `DataCon`s which include `Type`s, which mention `TyCon`s. 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8776#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8776: Displaying pattern synonym for a GADT -------------------------------------+------------------------------------ Reporter: monoidal | Owner: cactus Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Changes (by cactus): * owner: => cactus Comment: 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 `RealDataCon`s. If you think that makes sense, I can clean it up somewhat (by removing remnants of the old way to print `PatSynCon` `TyThing`s) and merge it to `master`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8776#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8776: Displaying pattern synonym for a GADT -------------------------------------+------------------------------------ Reporter: monoidal | Owner: cactus Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by simonpj): Gergo, Yes that looks right to me, thank you. Do remove the remnants and merge. 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. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8776#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8776: Displaying pattern synonym for a GADT -------------------------------------+------------------------------------ Reporter: monoidal | Owner: cactus Type: bug | Status: merge Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Changes (by cactus): * status: new => merge Comment: OK I've done all but `ATyCon`. It's merged into `master` and should be ready to be picked up into `ghc-7.8`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8776#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8776: Displaying pattern synonym for a GADT -------------------------------------+------------------------------------ Reporter: monoidal | Owner: cactus Type: bug | Status: merge Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by simonpj): Did you come across any particular obstacles with `TyCon`? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8776#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8776: Displaying pattern synonym for a GADT -------------------------------------+------------------------------------ Reporter: monoidal | Owner: cactus Type: bug | Status: merge Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8776#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8776: Displaying pattern synonym for a GADT -------------------------------------+------------------------------------ Reporter: monoidal | Owner: cactus Type: bug | Status: merge Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (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? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8776#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8776: Displaying pattern synonym for a GADT -------------------------------------+------------------------------------ Reporter: monoidal | Owner: cactus Type: bug | Status: merge Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (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... -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8776#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8776: Displaying pattern synonym for a GADT
-------------------------------------+------------------------------------
Reporter: monoidal | Owner: cactus
Type: bug | Status: merge
Priority: normal | Milestone:
Component: Compiler | Version: 7.7
Resolution: | Keywords:
Operating System: Unknown/Multiple | Architecture: Unknown/Multiple
Type of failure: None/Unknown | Difficulty: Unknown
Test Case: | Blocked By:
Blocking: | Related Tickets:
-------------------------------------+------------------------------------
Comment (by Dr. ERDI Gergo
#8776: Displaying pattern synonym for a GADT
-------------------------------------+------------------------------------
Reporter: monoidal | Owner: cactus
Type: bug | Status: merge
Priority: normal | Milestone:
Component: Compiler | Version: 7.7
Resolution: | Keywords:
Operating System: Unknown/Multiple | Architecture: Unknown/Multiple
Type of failure: None/Unknown | Difficulty: Unknown
Test Case: | Blocked By:
Blocking: | Related Tickets:
-------------------------------------+------------------------------------
Comment (by Dr. ERDI Gergo
#8776: Displaying pattern synonym for a GADT -------------------------------------+------------------------------------ Reporter: monoidal | Owner: cactus Type: bug | Status: merge Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by cactus): Simon, I've reverted the part of the change that tunneled `AnId`s 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8776#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8776: Displaying pattern synonym for a GADT -------------------------------------+------------------------------------ Reporter: monoidal | Owner: cactus Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Changes (by thoughtpolice): * status: merge => closed * resolution: => fixed Comment: This is all merged into 7.8. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8776#comment:17 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC