Opened 10 months ago

Closed 10 days ago

#14847 closed bug (fixed)

Inferring dependent kinds for non-recursive types

Reported by: simonpj Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.2.2
Keywords: TypeInType Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: polykinds/T14847
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page: https://ghc.haskell.org/trac/ghc/wiki/GhcKinds/KindInference

Description (last modified by simonpj)

Consider this

data Proxy k (a :: k) = MkProxy
data Proxy2 k a = MkP (Proxy k a)

which is discussed in a corner of the user manual.

Surprisingly, we reject Proxy2 -- but there is nothing difficult about inferring its kind. There would be if it was recursive -- but it isn't.

Simple solution: for non-recursive type declarations (we do SCC analysis so we know which these are) do not call getInitialKinds; instead, just infer the kind of the definition! Simple.

Warning: is this recursive?

data Proxy2 k a where
  MkP :: Proxy k a -> Proxy2 k a 

Presumably no more than the other definition. But currently we need Proxy2 in the environment during kind inference, because we kind-check the result type. That seems jolly odd and inconsistent. Needs more thought.

Similar questions for

data T a where
  T :: Int -> T Bool

type family F a where
  F Int = True
  F _   = False

See also:

Change History (6)

comment:1 Changed 10 months ago by simonpj

Description: modified (diff)

comment:2 Changed 10 months ago by kcsongor

Wiki Page: https://ghc.haskell.org/trac/ghc/wiki/GhcKinds/KindInference

comment:3 Changed 2 weeks ago by RyanGlScott

I think commit 2257a86daa72db382eb927df12a718669d5491f8 (Taming the Kind Inference Monster) fixed this ticket, since the following now compiles after that commit:

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

data Proxy k (a :: k) = MkProxy
data Proxy2 k a = MkP (Proxy k a)

data Proxy2' k a where
  MkP' :: Proxy k a -> Proxy2' k a

data T a where
  T :: Int -> T Bool

type family F a where
  F Int = True
  F _   = False

comment:4 Changed 10 days ago by simonpj

Yes, I think this is fixed. I'll add a test case. Thanks for spotting this

comment:5 Changed 10 days ago by Simon Peyton Jones <simonpj@…>

In 91c4e71f/ghc:

Tests Trac #14847

comment:6 Changed 10 days ago by simonpj

Resolution: fixed
Status: newclosed
Test Case: polykinds/T14847
Note: See TracTickets for help on using tickets.