#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