#11519 closed bug (fixed)

Inferring non-tau kinds

Reported by: goldfire Owned by:
Priority: normal Milestone: 8.0.1
Component: Compiler Version: 8.0.1-rc1
Keywords: TypeInType Cc: adamgundry
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

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 ExpTypes when kind-checking types. Then I think the normal bidirectional thing (actually already implemented) will do the Right Thing.

Change History (12)

comment:1 Changed 20 months ago by adamgundry

Cc: adamgundry added

I think it would be very sensible to permit type variable bindings in instance declarations. The syntax could be

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...):

instance pi (n :: Nat) . Monad (Vec n) where

comment:2 Changed 20 months ago by simonpj

Yes I think that using ExpTypes 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

comment:3 in reply to:  2 Changed 20 months ago by goldfire

Replying to simonpj:

Yes I think that using ExpTypes 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.

comment:4 Changed 20 months ago by simonpj

What sort of "doesn't work"? I'm losing the connection

comment:5 Changed 20 months ago by goldfire

The instance declaration with an explicit forall. And I just tried this, which is also rejected:

instance forall a. Eq (a -> a)

comment:6 Changed 20 months ago by Simon Peyton Jones <simonpj@…>

In 2cf3cac6/ghc:

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.

comment:7 Changed 20 months ago 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

comment:8 Changed 20 months ago 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?

comment:9 Changed 20 months ago by simonpj

I do not feel strongly

comment:10 Changed 20 months ago 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

comment:11 Changed 19 months ago by bgamari

Milestone: 8.0.1
Status: newmerge
Version: 8.18.0.1-rc1

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.

comment:12 Changed 19 months ago by bgamari

Resolution: fixed
Status: mergeclosed
Note: See TracTickets for help on using tickets.