[GHC] #15039: Bizarre pretty-printing of inferred Coercible constraint in partial type signature
#15039: Bizarre pretty-printing of inferred Coercible constraint in partial type signature -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.1 (Type checker) | Keywords: | Operating System: Unknown/Multiple PartialTypeSignatures | Architecture: | Type of failure: Poor/confusing Unknown/Multiple | error message Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Consider the following GHCi session: {{{ $ ghci GHCi, version 8.4.1: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci λ> import Data.Type.Coercion λ> foo :: _ => Coercion a b; foo = Coercion <interactive>:2:8: error: • Found type wildcard ‘_’ standing for ‘Coercible a b :: TYPE ('GHC.Types.TupleRep '[])’ Where: ‘a’, ‘b’ are rigid type variables bound by the inferred type of foo :: Coercible a b => Coercion a b at <interactive>:2:27-40 To use the inferred type, enable PartialTypeSignatures • In the type signature: foo :: _ => Coercion a b λ> :set -fprint-explicit-kinds λ> foo :: _ => Coercion a b; foo = Coercion <interactive>:4:8: error: • Found type wildcard ‘_’ standing for ‘(a :: *) ~~ (b :: *) :: TYPE ('GHC.Types.TupleRep ('[] GHC.Types.RuntimeRep))’ Where: ‘a’, ‘b’ are rigid type variables bound by the inferred type of foo :: ((a :: *) ~~ (b :: *)) => Coercion * a b at <interactive>:4:27-40 To use the inferred type, enable PartialTypeSignatures • In the type signature: foo :: _ => Coercion a b }}} There are two things quite strange about this: 1. In both error messages, GHC claims that `Coercible a b`/`a ~~ b` has kind `TYPE (TupleRep '[])`. This is wrong, and should be `Coercible`. 2. For some reason, enabling `-fprint-explicit-kinds` causes the inferred constraint to be `(~~)` instead of `Coercible`, which is just plain wrong. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15039 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15039: Bizarre pretty-printing of inferred Coercible constraint in partial type signature -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.4.1 checker) | Keywords: Resolution: | PartialTypeSignatures Operating System: Unknown/Multiple | Architecture: Type of failure: Poor/confusing | Unknown/Multiple error message | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): #15039 I know what is going on here. When we first introduced explicit equalities Richard arranged to make the pretty-printer conceal some of the menagerie, with some ad-hoc rules sketched in `IfaceType`: {{{ Note [Equality predicates in IfaceType] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ GHC has several varieties of type equality (see Note [The equality types story] in TysPrim for details). In an effort to avoid confusing users, we suppress the differences during "normal" pretty printing. Specifically we display them like this: Predicate Pretty-printed as Homogeneous case Heterogeneous case ---------------- ----------------- ------------------- (~) eqTyCon ~ N/A (~~) heqTyCon ~ ~~ (~#) eqPrimTyCon ~# ~~ (~R#) eqReprPrimTyCon Coercible Coercible By "homogeneeous case" we mean cases where a hetero-kinded equality (all but the first above) is actually applied to two identical kinds. Unfortunately, determining this from an IfaceType isn't possible since we can't see through type synonyms. Consequently, we need to record whether this particular application is homogeneous in IfaceTyConSort for the purposes of pretty-printing. All this suppresses information. To get the ground truth, use -dppr-debug (see 'print_eqs' in 'ppr_equality'). See Note [The equality types story] in TysPrim. }}} There's a flag to control this: `-fprint-equality-relations`, and using that flag makes both oddities go away. In this particular case, although it displays `Coercible a b`, it is really pretty printing `a ~R# b`! And that is why the kind looks wrong: it's the kind of `a ~R# b`. So concealing the reality is jolly confusing here. Moreover, for reasons I don't understand, `-fprint-explicit-kinds` affects the behhaviour too, hence oddness (2). It's all in `IfaceType.ppr_equality`, which I reproduce below {{{ ppr_equality :: TyPrec -> IfaceTyCon -> [IfaceType] -> Maybe SDoc ppr_equality ctxt_prec tc args | hetero_eq_tc , [k1, k2, t1, t2] <- args = Just $ print_equality (k1, k2, t1, t2) | hom_eq_tc , [k, t1, t2] <- args = Just $ print_equality (k, k, t1, t2) | otherwise = Nothing where homogeneous = case ifaceTyConSort $ ifaceTyConInfo tc of IfaceEqualityTyCon -> True _other -> False -- True <=> a heterogeneous equality whose arguments -- are (in this case) of the same kind tc_name = ifaceTyConName tc pp = ppr_ty hom_eq_tc = tc_name `hasKey` eqTyConKey -- (~) hetero_eq_tc = tc_name `hasKey` eqPrimTyConKey -- (~#) || tc_name `hasKey` eqReprPrimTyConKey -- (~R#) || tc_name `hasKey` heqTyConKey -- (~~) print_equality args = sdocWithDynFlags $ \dflags -> getPprStyle $ \style -> print_equality' args style dflags print_equality' (ki1, ki2, ty1, ty2) style dflags | print_eqs -- No magic, just print the original TyCon = ppr_infix_eq (ppr tc) | hetero_eq_tc , print_kinds || not homogeneous = ppr_infix_eq (text "~~") | otherwise = if tc_name `hasKey` eqReprPrimTyConKey then pprIfacePrefixApp ctxt_prec (text "Coercible") [pp TyConPrec ty1, pp TyConPrec ty2] else pprIfaceInfixApp ctxt_prec (char '~') (pp TyOpPrec ty1) (pp TyOpPrec ty2) where ppr_infix_eq eq_op = pprIfaceInfixApp ctxt_prec eq_op (parens (pp TopPrec ty1 <+> dcolon <+> pp TyOpPrec ki1)) (parens (pp TopPrec ty2 <+> dcolon <+> pp TyOpPrec ki2)) print_kinds = gopt Opt_PrintExplicitKinds dflags print_eqs = gopt Opt_PrintEqualityRelations dflags || dumpStyle style || debugStyle style }}} What to do? I'm not sure. But that's what is going on. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15039#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15039: Bizarre pretty-printing of inferred Coercible constraint in partial type signature -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.4.1 checker) | Keywords: Resolution: | PartialTypeSignatures, TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: Poor/confusing | Unknown/Multiple error message | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: PartialTypeSignatures => PartialTypeSignatures, TypeInType -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15039#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15039: Bizarre pretty-printing of inferred Coercible constraint in partial type signature -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.4.1 checker) | Keywords: Resolution: | PartialTypeSignatures, TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: Poor/confusing | Unknown/Multiple error message | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Well, that's one half of the mystery (2). Do you know why (1) is happening? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15039#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15039: Bizarre pretty-printing of inferred Coercible constraint in partial type signature -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.4.1 checker) | Keywords: Resolution: | PartialTypeSignatures, TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: Poor/confusing | Unknown/Multiple error message | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): The idea is that, with `-fprint-explicit-kinds`, `(a ~~ b)` should be printed as `((a :: *) ~~ (b :: *))`, with the explicit kinds. But `(a ~# b)` should ''also'' be printed as `((a :: *) ~~ (b :: *))`, so as not to expose the user to `~#`. Note that `(a ~ b)` is just printed as `(a ~ b)`, even with `-fprint-explicit-kinds`, which seems wrong. And, of course, `~R#` should never be printed with `~~`. What to do? Here are the cases. Assume `a :: *`, `b :: *`, and `c :: k`. 1. Homogeneous equality `a ~ b`. 2. Homogeneous use of heterogeneous equality `a ~~ b`. 3. Heterogeneous use of heterogeneous equality `a ~~ c`. 4. Homogeneous use of unlifted equality `a ~# b`. 5. Heterogeneous use of unlifted equality `a ~# c`. 6. Homegeneous representational equality `Coercible a b`. 7. Homogeneous use of representational unlifted equality `a ~#R b`. 8. Heterogeneous use of representational unlifted equality `a ~R# c`. Note that there is no heterogeneous representational lifted equality (the counterpert to `~~`). There could be, but there seems to be no use for it. For each case, we must decide how to print a. By default b. With `-fprint-explicit-kinds` c. With `-fprint-equality-relations` d. With `-fprint-explicit-kinds -fprint-equality-relations`. I propose: 1. a. `a ~ b` b. `(a :: *) ~ (b :: *)` c. `a ~ b` d. `(a :: *) ~ (b :: *)` 2. a. `a ~ b` b. `(a :: *) ~ (b :: *)` c. `a ~~ b` d. `(a :: *) ~~ (b :: *)` 3. a. `a ~~ c` b. `(a :: *) ~~ (c :: k)` c. `a ~~ c` d. `(a :: *) ~~ (c :: k)` 4. a. `a ~ b` b. `(a :: *) ~ (b :: *)` c. `a ~# b` d. `(a :: *) ~# (b :: *)` 5. a. `a ~~ c` b. `(a :: *) ~~ (c :: k)` c. `a ~# c` d. `(a :: *) ~# (c :: k)` 6. a. `Coercible a b` b. `Coercible * a b` c. `Coercible a b` d. `Coercible * a b` 7. a. `Coercible a b` b. `Coercible * a b` c. `a ~R# b` d. `(a :: *) ~R# (b :: *)` 8. a. `a ~R# c` b. `(a :: *) ~R# (c :: k)` c. `a ~R# c` d. `(a :: *) ~R# (c :: k)` Here are the rules: A. With `-fprint-equality-relations`, print the true equality relation. B. Without `-fprint-equality-relations`: i. If the equality is representational and homogeneous, use `Coercible`. ii. Otherwise, if the equality is representational, use `~R#`. iii. If the equality is nominal and homogeneous, use `~`. iv. Otherwise, if the equality is nominal, use `~~`. C. With `-fprint-explicit-kinds`, print kinds on both sides of an infix operator, as above; or print the kind with `Coercible`. D. Without `-fprint-explicit-kinds`, don't print kinds. I believe that my examples above conform to these rules. Do we agree with this approach? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15039#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15039: Bizarre pretty-printing of inferred Coercible constraint in partial type signature -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.4.1 checker) | Keywords: Resolution: | PartialTypeSignatures, TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: Poor/confusing | Unknown/Multiple error message | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): That looks good to me. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15039#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15039: Bizarre pretty-printing of inferred Coercible constraint in partial type signature -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.4.1 checker) | Keywords: Resolution: | PartialTypeSignatures, TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: Poor/confusing | Unknown/Multiple error message | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): comment:5 sounds fine, but it only addresses problem (2). What about problem (1)? We still have GHC reporting that the kind of `Coercible a b` is `TYPE (TupleRep '[])`, which is utterly bogus. It seems like if `-fprint-equality-relations` is disabled, then we'd want to print the kind `Constraint` instead, yes? Is that feasible with the way partial type signature reporting currently works? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15039#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15039: Bizarre pretty-printing of inferred Coercible constraint in partial type signature -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.4.1 checker) | Keywords: Resolution: | PartialTypeSignatures, TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: Poor/confusing | Unknown/Multiple error message | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I think comment:6 is a red herring. Why is GHC attempting to report about `~R#` at all here? The type of the hole is really `Coercible a b`. I don't think this is a pretty-printing issue. Instead, the solver needs to be taught somewhere to transmute `a ~R# b` constraints to `Coercible a b` constraints. But where? Do we do this for nominal equality anywhere? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15039#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15039: Bizarre pretty-printing of inferred Coercible constraint in partial type signature -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.4.1 checker) | Keywords: Resolution: | PartialTypeSignatures, TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: Poor/confusing | Unknown/Multiple error message | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):
Instead, the solver needs to be taught somewhere to transmute a ~R# b constraints to Coercible a b constraints. But where? Do we do this for nominal equality anywhere?
We do not transmute unsolved `a ~# b` constraints into `a ~ b`. Rather we ''pretty-print'' the unsolved `a ~# b` constraint as `a ~ b`. But if we do that ''and'' print the kind of the constraint, the two will be inconsistent. It appears that this only shows up for holes. Maybe we should refrain from printing the kind of a hole-filler if it's a constraint? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15039#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15039: Bizarre pretty-printing of inferred Coercible constraint in partial type signature -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.4.1 checker) | Keywords: Resolution: | PartialTypeSignatures, TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: Poor/confusing | Unknown/Multiple error message | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D4696 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => patch * differential: => Phab:D4696 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15039#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15039: Bizarre pretty-printing of inferred Coercible constraint in partial type
signature
-------------------------------------+-------------------------------------
Reporter: RyanGlScott | Owner: (none)
Type: bug | Status: patch
Priority: normal | Milestone: 8.6.1
Component: Compiler (Type | Version: 8.4.1
checker) | Keywords:
Resolution: | PartialTypeSignatures, TypeInType
Operating System: Unknown/Multiple | Architecture:
Type of failure: Poor/confusing | Unknown/Multiple
error message | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s): Phab:D4696
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Ben Gamari
#15039: Bizarre pretty-printing of inferred Coercible constraint in partial type signature -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.4.1 checker) | Keywords: Resolution: fixed | PartialTypeSignatures, TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: Poor/confusing | Unknown/Multiple error message | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D4696 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: patch => closed * cc: partial-sigs/should_compile/T15039a, partial- sigs/should_compile/T15039b, partial-sigs/should_compile/T15039c, partial- sigs/should_compile/T15039d (added) * resolution: => fixed -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15039#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC