#8707: Kind inference fails in data instance definition -------------------------------------+------------------------------------ Reporter: goldfire | 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: -------------------------------------+------------------------------------ Changes (by jstolarek): * cc: jan.stolarek@… (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8707#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8707: Kind inference fails in data instance definition -------------------------------------+------------------------------------ Reporter: goldfire | Owner: jstolarek 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 jstolarek):

2) The error message is not particularly helpful. GHC 7.6.3 had a more verbose, but more helpful message.

Code responsible for this difference is here [[GhcFile(compiler/types/TypeRep.lhs#L711)]] in the function `pprTcApp`: {{{ | Just dc <- isPromotedDataCon_maybe tc , let dc_tc = dataConTyCon dc , isTupleTyCon dc_tc , let arity = tyConArity dc_tc -- E.g. 3 for (,,) k1 k2 k3 t1 t2 t3 ty_args = drop arity tys -- Drop the kind args , ty_args `lengthIs` arity -- Result is saturated = pprPromotionQuote tc <> (tupleParens (tupleTyConSort dc_tc) $ sep (punctuate comma (map (pp TopPrec) tys))) }}} The only question is how we want the arguments printed? GHC 7.6 prints them like this: {{{ Data constructor `SFalse' returns type `SingDF Bool k ('(,) Bool (k -> *) 'False (Ctor k))' instead of an instance of its parent type `SingDF Bool Bool a' }}} GHC HEAD prints tuple constructors in the standard notation (not prefix as seen in GHC 7.6 output): {{{ Data constructor ‘SFalse’ returns type ‘SingDF Bool k '(Bool, k -> *, 'False, Ctor k)’ instead of an instance of its parent type ‘SingDF Bool Bool a’ }}} But printing kinds as part of a tuple is misleading. Any suggestions how should the output look like? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8707#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8707: Kind inference fails in data instance definition -------------------------------------+------------------------------------ Reporter: goldfire | Owner: jstolarek 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 jstolarek): Replying to [comment:4 simonpj]:

Jan, how did you manage to get GHC to produce this? {{{ Data constructor `SFalse' returns type `SingDF Bool k ('(,) Bool (k -> *) 'False (Ctor k))' }}} That does look wrong. Can you explain how to reproduce it? That is part of error message produced by GHC 7.6.3. As for this output:

{{{ Data constructor ‘SFalse’ returns type ‘SingDF Bool k '(Bool, k -> *, 'False, Ctor k)’ }}} I made a quick hack in `pprTcApp` and replaced `ty_args = drop arity tys` with `ty_args = tys`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8707#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8707: Kind inference fails in data instance definition -------------------------------------+------------------------------------ Reporter: goldfire | Owner: jstolarek 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): Richard, re (1), here's my analysis * For ordinary GADTs we first figure out the kind of the type constructor, and only then typecheck the constructor types. So this works fine: {{{ data SingDF (a :: (Bool, Bool -> *)) where SFalse :: SingDF '(False, Ctor) }}} We figure out the kind `SingDF :: (Bool, Bool -> *) -> *`, and only then typecheck the type of `SFalse`. So the use of `SingDF` in the type of the data constructor is fine. * But for a data family, the kind of the type constructor is polymorphic, in this case `SingDF :: forall k1,k1. (k1, k2 -> *) -> *`. When we use this kind in type-checking the type of `SFalse` we don't get any info from the `data instance` header. * And indeed if `SingDF` was used in a constructor ''argument'' we would want the polymorphic version: {{{ data instance SingDF (a :: (Bool, Bool) -> *) where SFalse :: SingDF (...blah...) -> SingDF '(False, Ctor) }}} Here the `(...blah...)` need not have kind `(Bool,Bool) -> *`. * So if we are to use the `data instance` header to inform the kind of the quantified type variables in the data constructor(s), we must treat the result type specially (`TcTyClsDecls.tcConRes`). * Currently we simply use `tcHsLiftedType`. I think to do the Right Thing we would need a special version of `TcHsType.tc_lhs_type`, expecially for data constructor result types. And this might be a Good Thing. Although it would mean a little code duplication, it might eliminate much of the delicacy in `Note [Checking GADT return types]` This is a bit of code you know quite well. Happy to discuss. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8707#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8707: Kind inference fails in data instance definition -------------------------------------+------------------------------------ Reporter: goldfire | Owner: jstolarek 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 goldfire): Replying to [comment:6 simonpj]:

Oh oh, so that message is not something can currently produce. Fine. Then my question remains: what's wrong with the status quo, for question (2)?

Nothing, upon further inspection. I believe I wrote that message toward the end of a 6-hour flight and may have been a little addled. I withdraw point (2). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8707#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8707: Kind inference fails in data instance definition -------------------------------------+------------------------------------ Reporter: goldfire | Owner: jstolarek 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 goldfire): Jan asked me a few months ago for a "simple" bug to fix in the type- checker, and I recommended this one, thinking it to be much simpler than it is -- that's why I haven't tackled it myself. He and I just spent a some time going through the details, and we hit upon a much simpler solution than what you proposed. Right now, `tcConRes` looks like this: {{{ tcConRes (ResTyGADT res_ty) = do { res_ty' <- tcHsLiftedType res_ty ; return (ResTyGADT res_ty') } }}} I propose changing it to: {{{ tcConRes (ResTyGADT res_ty) = do { res_ty' <- tcHsLiftedType res_ty ; _ <- unifyType type_in_head res_ty' ; return (ResTyGADT res_ty') } }}} where `type_in_head` is the desugared type that appears in the declaration (either normal datatype or data instance) head. Getting that data here will take some plumbing, but it shouldn't be too bad. We also will need to freshen any type variables (with `tcInstTyVars` for the type from the declaration head and `tcInstSkolTyVars` for the return type, I imagine) to get everything to work. This approach seems to solve the case in point, and it would also fix the complications in `Note [Checking GADT return types]`. I do see some potential trouble with getting error messages to be right, but I still think this is a better approach than repeating much of `tc_hs_type`. Thoughts? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8707#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8707: Kind inference fails in data instance definition -------------------------------------+------------------------------------ Reporter: goldfire | Owner: jstolarek 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 goldfire): Quite right. But, your comment about the fact that this works for data instances gives me an idea: what about doing this unification in `kcDataDefn`? Note that the function is used only in the data instance case. (It might be worth renaming to make this now-critical fact more obvious.) There's no knot to worry about there. `kcConDecl` would be rewritten to return the desugared result type so that `kcDataDefn` can access it. Should be rather straightforward. If you agree that this might work, the question now is: is it better to have this (admittedly somewhat delicate) check in addition to the already- delicate handling of GADT return types? Or is it better to have a duplication of all the work in `tc_hs_type`? If we go with duplicating `tc_hs_type`, it's not immediately obvious exactly how the GADT-return- type typechecker would operate, given that the constraints on that type may appear arbitrarily deep in the type, depending on the data instance type patterns. I'm sure there's a way to get it to work, but I have a sneaking suspicion it will look a lot like a call to `unifyType` somewhere. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8707#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8707: Kind inference fails in data instance definition -------------------------------------+------------------------------------ Reporter: goldfire | Owner: jstolarek Type: feature request | Status: new Priority: low | 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 goldfire): Given the (current) separation between types and kinds, I'm not 100% convinced that the `SingDF` case is the same as your `T` case, but I can see how these might become the same in the future. I agree with the reclassification as a feature request, and that there are bigger fish to fry, so I agree to table this one. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8707#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8707: Kind inference fails in data instance definition -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: feature request | Status: new Priority: low | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by jstolarek): * cc: jan.stolarek@… (removed) * cc: jstolarek (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8707#comment:17 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler