[GHC] #15827: Explicit foralls in type family equations are pretty-printed inconsistently (and strangely, at times)
#15827: Explicit foralls in type family equations are pretty-printed inconsistently (and strangely, at times) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.7 Keywords: TypeFamilies | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Load the following code into GHCi HEAD (8.7+): {{{#!hs {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} module Bug where import Data.Kind type family F1 a type instance forall a. F1 a = Maybe a type family F2 a where forall a. F2 a = Maybe a data family D a data instance forall a. D a = MkD (Maybe a) }}} And make sure you have the `-fprint-explicit-foralls` flag enabled. Now let's see what happens when we look up the `:info` for each of these type families: {{{ $ ~/Software/ghc2/inplace/bin/ghc-stage2 --interactive Bug.hs -fprint- explicit-foralls GHCi, version 8.7.20181029: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) Ok, one module loaded. λ> :i F1 type family F1 a :: * -- Defined at Bug.hs:7:1 type instance F1 a = Maybe a -- Defined at Bug.hs:8:25 λ> :i F2 type family F2 a :: * where [a] F2 a = Maybe a -- Defined at Bug.hs:10:1 λ> :i D data family D a -- Defined at Bug.hs:13:1 data instance D a = MkD (Maybe a) -- Defined at Bug.hs:14:25 }}} There are two strange things of note here: * The equations for `F1` and `D` do not have any explicit `forall`s displayed at all, despite the fact that `-fprint-explicit-foralls` is enabled. * The equation for `F2` //does// have an explicit `forall` displayed, but in a rather bizarre fashion: {{{ λ> :i F2 type family F2 a :: * where [a] F2 a = Maybe a -- Defined at Bug.hs:10:1 }}} I certainly wasn't expecting to see the type variables in square brackets. I would have hoped to see something like this instead: {{{ λ> :i F2 type family F2 a :: * where forall a. F2 a = Maybe a -- Defined at Bug.hs:10:1 }}} Now that the "more explicit `forall`s" proposal is implemented, my hope is that it will be somewhat simple to change the way that this is pretty- printed (we already store the explicit `forall` information within the AST, after all). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15827 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15827: Explicit foralls in type family equations are pretty-printed inconsistently (and strangely, at times) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.7 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Hm, it appears that fixing this may not be as straightforward as I would have hoped. The main issue that I encountered is that `:info` displays type family equations by first converting them to their interface file equivalents and then pretty-printing them. Take a look at [http://git.haskell.org/ghc.git/blob/4427315a65b25db22e1754d41b43dd4b782b022f... IfaceAxBranch] (which is the interface file incarnation of a type family equation), for instance: {{{#!hs data IfaceAxBranch = IfaceAxBranch { ifaxbTyVars :: [IfaceTvBndr] , ifaxbCoVars :: [IfaceIdBndr] , ... } }}} Notice that this stores type variable information (`ifaxbTyVars`) as `IfaceTvBndr`s instead of `IfaceTyConBinder`s. This is an important distinction because essentially all of the machinery within `IfaceType` that pretty-prints explicit `forall`s works over `IfaceTyConBinder`s, not `IfaceTvBndr`s. (This makes some amount of sense since an `IfaceTyConBinder` stores visibility information but an `IfaceTvBinder` does not.) I suppose that we could just convert the `ifaxbTyVars` to `IfaceTyConBinder`s (defaulting each variable's visibility to specified) before pretty-printing. But there's another challenge: how should we print the `ifaxbCoVars`? The [http://git.haskell.org/ghc.git/blob/4427315a65b25db22e1754d41b43dd4b782b022f... existing code] for pretty-printing `IfaceAxBranch`es actually does take `ifaxbCoVars` into account at the moment: {{{#!hs pprAxBranch pp_tc (IfaceAxBranch { ifaxbTyVars = tvs , ifaxbCoVars = cvs , ifaxbLHS = pat_tys , ifaxbRHS = rhs , ifaxbIncomps = incomps }) = hang ppr_binders 2 (hang pp_lhs 2 (equals <+> ppr rhs)) $+$ nest 2 maybe_incomps where ppr_binders = sdocWithDynFlags $ \dflags -> ppWhen (gopt Opt_PrintExplicitForalls dflags) ppr_binders' ppr_binders' | null tvs && null cvs = empty | null cvs = brackets (pprWithCommas (pprIfaceTvBndr True) tvs) | otherwise = brackets (pprWithCommas (pprIfaceTvBndr True) tvs <> semi <+> pprWithCommas pprIfaceIdBndr cvs) }}} I'm not sure what this code should become if we start using the `forall` keyword instead. To make things even more confusing, the [http://git.haskell.org/ghc.git/blob/4427315a65b25db22e1754d41b43dd4b782b022f... comments] for `CoAxBranch`: {{{#!hs data CoAxBranch = CoAxBranch { ... , cab_tvs :: [TyVar] -- Bound type variables; not necessarily fresh -- See Note [CoAxBranch type variables] -- May be eta-reduded; see FamInstEnv -- Note [Eta reduction for data families] , cab_cvs :: [CoVar] -- Bound coercion variables -- Always empty, for now. -- See Note [Constraints in patterns] -- in TcTyClsDecls , ... } }}} Suggest that the bound coercion variables in a coaxiom branch are always empty in practice! So is it even worth fretting over them? Perhaps an expert in this area could answer this question, but I'm far from that expert. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15827#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15827: Explicit foralls in type family equations are pretty-printed inconsistently (and strangely, at times) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.7 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): The covars are always empty. That comment is right. Along the way to `-XTypeInType`, there were some scenarios where the covars weren't empty. Mutterings to self are memorialized [https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Internal#Matchingaxio... here]. As for pretty-printing behavior, I have a few observations: - The AST indeed stores whether or not the user wrote a `forall`, because some of the warnings, etc., are different based on this choice. However, once a type family equation is accepted, the presence/absence of the `forall` is immaterial. - The order of variables in the `forall` is immaterial to users. Not sure if this is a problem at all, but there's never a way to manually instantiate the variables, so we don't have to care about order. - Visibility/specificity is simply not a thing for the variables bound in a type family equation, also because the user can't ever instantiate these manually. - The funny `[a]` syntax was invented because using `forall` here is a tiny bit of a lie: `forall` is a specific construct in Core that does not exist in type family equations (i.e. coercion axioms). I don't think this is useful or friendly to users, though. Do these design points help? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15827#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15827: Explicit foralls in type family equations are pretty-printed inconsistently (and strangely, at times) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.7 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): OK. In that case, my tentative plan is to: * Not print the coercion variables at all. * Pretty-print the type variables by first converting them to `IfaceForAllBinder`s (defaulting their visibilities to specified //à la// `mkSpecForAllTys`) and then using a function like `pprIfaceForAll` to pretty-print them with the explicit `forall` syntax. Does that sound reasonable? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15827#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15827: Explicit foralls in type family equations are pretty-printed inconsistently (and strangely, at times) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.7 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Yes. Without looking at the implementation, I'm not sure: will this print the kind of the type variables whose kind is not `Type`? If so (as I imagine it is), then full speed ahead. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15827#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15827: Explicit foralls in type family equations are pretty-printed inconsistently (and strangely, at times) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.7 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D5282 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => patch * differential: => Phab:D5282 * milestone: => 8.8.1 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15827#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15827: Explicit foralls in type family equations are pretty-printed inconsistently
(and strangely, at times)
-------------------------------------+-------------------------------------
Reporter: RyanGlScott | Owner: (none)
Type: bug | Status: patch
Priority: normal | Milestone: 8.8.1
Component: Compiler | Version: 8.7
Resolution: | Keywords: TypeFamilies
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: None/Unknown | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s): Phab:D5282
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Ryan Scott
#15827: Explicit foralls in type family equations are pretty-printed inconsistently (and strangely, at times) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.7 Resolution: fixed | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | ghci/scripts/T15827 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D5282 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * testcase: => ghci/scripts/T15827 * status: patch => closed * resolution: => fixed -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15827#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC