[GHC] #11519: Inferring non-tau kinds
#11519: Inferring non-tau kinds -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Keywords: TypeInType | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- While up to my usual type-level shenanigans, I found that I want this definition: {{{ data TypeRep (a :: k) -- abstract data TypeRepX :: (forall k. k -> Constraint) -> Type where TypeRepX :: forall k (c :: forall k'. k' -> Constraint) (a :: k). c a => TypeRep a -> TypeRepX c }}} Note `TypeRepX`'s higher-rank kind. The idea is that I want to optionally constrain `TypeRepX`'s payload. Without using a higher-rank kind, the constraint would necessary fix the kind of the payload, and I don't want that. For example, I sometimes use `TypeRepX ConstTrue`, where {{{ class ConstTrue (a :: k) instance ConstTrue a }}} This actually works just fine, and I've been using the above definition to good effect. But then I wanted a `Show` instance: {{{ instance Show (TypeRep a) -- elsewhere instance Show (TypeRepX c) where show (TypeRepX tr) = show t }}} Looks sensible. But GHC complains. This is because it tries to infer `c`'s kind, by inventing a unification variable and then unifying. But this doesn't work, of course, because `c`'s kind is not a tau-type, so unification fails, lest we let impredicativity sneak in. What's particularly vexing is that, even if I annotate `c` with the correct kind, unification ''still'' fails. This is because that `c` is a ''usage'' of `c`, not a ''binding'' of `c`. Indeed, there is no place in an instance declaration to bind a type variable explicitly, so I have no recourse. I'm not sure what the solution is here. Somehow, it feels that inferring a non-tau kind for `c` is perfectly safe, because the kind is known from the use of `TypeRepX`. This would allow me to drop the kind annotation in the definition of `TypeRepX`, which looks redundant to me. But I'm not fully sure about this assumption. At the least, we could introduce a spot for explicit binding of type variables in instance declarations. I think, actually, I just figured it out. Use `ExpType`s when kind- checking types. Then I think the normal bidirectional thing (actually already implemented) will do the Right Thing. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11519> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11519: Inferring non-tau kinds -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by adamgundry): * cc: adamgundry (added) Comment: I think it would be very sensible to permit type variable bindings in instance declarations. The syntax could be {{{#!hs instance forall (c :: forall k . k -> Constraint) . Show (TypeRepX c) where }}} which is hardly beautiful, but gets the job done. My thesis had another example of this need (if we had a `pi` quantifier, of course...): {{{#!hs instance pi (n :: Nat) . Monad (Vec n) where }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11519#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11519: Inferring non-tau kinds -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: TypeInType 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 simonpj): Yes I think that using `ExpType`s is exactly the right thing here. Interestingly we used to have a variant of `ExpType`, called `ExpKind`: {{{ data ExpKind = EK TcKind (TcKind -> SDoc) }}} but that has gone now. I'm not sure how you managed to keep the error messages good without that `SDoc` argument, but I'm all for the simplification. So now perhaps `ExpType` will do just fine. I also agree with Adam about explicit quantification. (Both are independently useful.) And in fact I think that the declaration he give is accepted already -- an entirely un-documented feature. Adding some docs for it would be good. Simon -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11519#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11519: Inferring non-tau kinds -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: TypeInType 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): Replying to [comment:2 simonpj]:
Yes I think that using `ExpType`s is exactly the right thing here. Interestingly we used to have a variant of `ExpType`, called `ExpKind`: {{{ data ExpKind = EK TcKind (TcKind -> SDoc) }}} but that has gone now. I'm not sure how you managed to keep the error messages good without that `SDoc` argument, but I'm all for the simplification.
That was actually quite a bit of work. All the kind errors used to be reported eagerly, during constraint generation. Thus the `SDoc` argument came into play. Now kind errors are naturally reported from !TcErrors, so the `ExpKind` stuff doesn't work. Instead, look at `mkExpectedActualMsg`, which re-creates the old messages. You might notice that the function is a terrible mess.... I would love to find a theory or specification of error messages against which we can write an implementation. Because !TcErrors is inscrutable. I made it considerably worse, but it wasn't in that good a state when I arrived. In any case, that's where the error messages have gone.
So now perhaps `ExpType` will do just fine.
I also agree with Adam about explicit quantification. (Both are
independently useful.) And in fact I think that the declaration he give is accepted already -- an entirely un-documented feature. Adding some docs for it would be good. I actually seem to recall implementing something along these lines once upon a time. But the following full module doesn't work for me: {{{ {-# LANGUAGE RankNTypes, TypeInType, GADTs, ConstraintKinds #-} module Bug where import GHC.Exts import Data.Kind data TypeRep (a :: k) -- abstract data TypeRepX :: (forall k. k -> Constraint) -> Type where TypeRepX :: forall k (c :: forall k'. k' -> Constraint) (a :: k). c a => TypeRep a -> TypeRepX c instance Show (TypeRep a) -- elsewhere instance forall (c :: forall k. k -> Constraint). Show (TypeRepX c) where show (TypeRepX tr) = show t }}} Is there something I'm missing? I haven't looked at the GHC code for instance declarations. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11519#comment:3> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11519: Inferring non-tau kinds -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: TypeInType 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 simonpj): What sort of "doesn't work"? I'm losing the connection -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11519#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11519: Inferring non-tau kinds -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: TypeInType 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 instance declaration with an explicit forall. And I just tried this, which is also rejected: {{{ instance forall a. Eq (a -> a) }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11519#comment:5> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11519: Inferring non-tau kinds -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: TypeInType 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 Simon Peyton Jones <simonpj@…>): In [changeset:"2cf3cac6a05879c27fa82b12dd34cce39a262402/ghc" 2cf3cac6/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="2cf3cac6a05879c27fa82b12dd34cce39a262402" Allow foralls in instance decls This patch finally makes it possible to have explicit foralls in an instance decl instance forall (a :: *). Eq a => Eq [a] where ... This is useful to allow kind signatures or indeed explicicit kind for-alls; see Trac #11519 I thought it would be really easy, because an instance declaration already contains an actual HsSigType, so all the syntactic baggage is there. But in fact it turned out that instance declarations were kind-checked a little differently, because the body kind of the forall is 'Constraint' rather than '*'. So I fixed that. There a slight kludge (see Note [Body kind of a HsQualTy], but it's still a significant improvement. I also did the usual other round of refactoring, improved a few error messages, tidied up comments etc. The only significant aspect of all that was * Kill mkNakedSpecSigmaTy, mkNakedPhiTy, mkNakedFunTy These function names suggest that they do something complicated, but acutally they do nothing. So I killed them. * Swap the arg order of mkNamedBinder, just so that it is convenient to say 'map (mkNamedBinder Invisible) tvs' * I had to improve isPredTy, to deal with (illegal) types like (Eq a => Eq [a]) => blah See Note [isPeredTy complications] in Type.hs Still to come: user manual documentation for the instance-decl change. }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11519#comment:6> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11519: Inferring non-tau kinds -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: TypeInType 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 simonpj): This doesn't close the ticket, but the above commit does now allow explicit quantification in instance decls, like comment:5. c.f. # 11552 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11519#comment:7> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11519: Inferring non-tau kinds -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: TypeInType 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 bgamari): Just to confirm: explicit instance foralls will be a an 8.2 feature and should not be merged to 8.0.1, correct? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11519#comment:8> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11519: Inferring non-tau kinds -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: TypeInType 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 simonpj): I do not feel strongly -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11519#comment:9> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11519: Inferring non-tau kinds -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: TypeInType 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 simonpj): This documents the instance-forall extension {{{ commit 6cf9b06fd193867bf4964eff4317479b9e25fca5 Author: Simon Peyton Jones <simonpj@microsoft.com> Date: Fri Feb 12 14:38:22 2016 +0000 User manual improvments - Document that you can use 'forall' in instance decls - Change the sections a bit, so that big sections (like lexically scoped type variables, pattern synonyms, implicit parameters) become more visible }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11519#comment:10> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11519: Inferring non-tau kinds -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: merge Priority: normal | Milestone: 8.0.1 Component: Compiler | Version: 8.0.1-rc1 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * status: new => merge * version: 8.1 => 8.0.1-rc1 * milestone: => 8.0.1 Comment: Alright, it can go in, if for no other reason than to keep `ghc-8.0` from diverging from `master` even more than it (already!) has. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11519#comment:11> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11519: Inferring non-tau kinds -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: closed Priority: normal | Milestone: 8.0.1 Component: Compiler | Version: 8.0.1-rc1 Resolution: fixed | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * status: merge => closed * resolution: => fixed Comment: Merged to `ghc-8.0` in 28c26d9da990e4889f77b562fb76fb79e71f9ef2 and c0e380f2a0c5f476d2aabc55a98f237c3b5c3021. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11519#comment:12> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
participants (1)
-
GHC