Opened 5 months ago

Last modified 6 weeks ago

#13407 new bug

Fix printing of higher-rank kinds

Reported by: goldfire Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.0.1
Keywords: TypeInType Cc:
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

Witness this GHCi session:

rae:09:18:37 ~/ghc/ghc> ghci -ignore-dot-ghci
GHCi, version 8.0.1: http://www.haskell.org/ghc/  :? for help
Prelude> :set -XTypeInType -XRankNTypes
Prelude> import Data.Kind
Prelude Data.Kind> data Foo :: (* -> *) -> (forall k. k -> *)
Prelude Data.Kind> :info Foo
type role Foo phantom nominal phantom
data Foo (a :: * -> *) k (c :: k)
  	-- Defined at <interactive>:3:1

The output from :info is terrible, treating k as a visible parameter when it isn't.

This is spun off from #13399 but is not tightly coupled to that ticket.

Change History (3)

comment:1 Changed 3 months ago by Iceland_jack

May relate to #12102, according to Ryan.

comment:2 Changed 6 weeks ago by RyanGlScott

Another higher-rank kind pretty-printing oddity:

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where

import Data.Kind

type family Foo (a :: Type) :: Type
type instance Foo (a :: forall k. k -> Type) = Int
GHCi, version 8.2.0.20170523: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )

Bug.hs:9:19: error:
    • Expecting one more argument to ‘a k1’
      Expected a type, but ‘a k1’ has kind ‘k1 -> *’
    • In the first argument of ‘Foo’, namely
        ‘(a :: forall k. k -> Type)’
      In the type instance declaration for ‘Foo’
  |
9 | type instance Foo (a :: forall k. k -> Type) = Int
  |                   ^^^^^^^^^^^^^^^^^^^^^^^^^^

The error message mentions a k1... how did that k1 sneak in there?

I'm not sure if it's due to the same root cause as the original issue, but thought it was worth mentioning.

comment:3 Changed 6 weeks ago by simonpj

Remember that teh arguments in a type instance are types, not type variables. So when you write

type instance Foo (a :: forall k. k-> TYpe) = ...

GHC treats it much like

-- Suppose T :: forall k. k -> Type

type instance Foo T = ...

It'll instantaite T's kind to give T k1 (where k1 is a unification variable. Then it'll to unify k1->Type with the expected argument kind of F, namely Type. Hence the error mesage.

Th eoddity is that it prints a k1 rather than just a even without fprint-explicit-kinds. I expect that's because the head isn't at type constructor, but rather a type variable -- a pretty-printing bug. But a palpable bug, I think.

Note: See TracTickets for help on using tickets.