Opened 3 months ago

Closed 3 months ago

#15987 closed bug (duplicate)

GHC sometimes not computing open type family application in kind inference

Reported by: sheaf Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.6.2
Keywords: Cc: Iceland_jack
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: #12088, #12643, #14668, #15561 Differential Rev(s):
Wiki Page:

Description

In writing code for type-level lenses, I've run into an issue with kind inference. I've boiled it down to the following oddity:

{-# LANGUAGE DataKinds    #-}
{-# LANGUAGE PolyKinds    #-}
{-# LANGUAGE TypeFamilies #-}

module Bug where 

import Data.Kind(Type)

type family FooKind (a :: Type) :: k
class Foo (a :: Type) where
  type FooType a :: FooKind a

-- OK
type instance FooKind Bool = Type
instance Foo Bool where
  type FooType Bool = Int

-- not OK
data A
type instance FooKind A = Type
instance Foo A where
  type FooType A = Int

This produces the following error:

  • Expected kind ‘FooKind A’, but ‘Int’ has kind ‘Type’
  • In the type ‘Int’ In the type instance declaration for ‘FooType’ In the instance declaration for ‘Foo A’

I thought it might be related to the type family FooKind being polymorphic in its return kind, but changing the return kind to 'Type' does not affect this.
Changing "FooKind" to be a closed type family fixes this problem.




For the context in which this came up, I was writing type-level optics of which one can take the product (with disjointness guaranteed at the type level with type families). Then I needed a type family that chooses which product to use. For instance I have kind annotations:

(     (Index 0 :: Optic (V Int 3) Int)
  :*: (Index 2 :: Optic (V Int 3) Int)
      ) :: Optic (V Int 3) (V Int 2) )

type Fields = '[ '("a", Int), '("b", Bool), '("c", Float) ]
(     (Name "a" :: Optic (Struct Fields) Int
  :*: (Name "c" :: Optic (Struct Fields) Float
      ) :: Optic Fields '[ '("a", Int), '("c", Float) ]

The type family :*: thus needs to figure out which product structure to use... in the first case I need to use V Int :: Nat -> Type, and in the second Struct :: [(Symbol,Type)] -> Type.
I wanted to use open type families for extensibility of which cartesian structure to use.

Change History (4)

comment:1 Changed 3 months ago by Iceland_jack

Cc: Iceland_jack added

comment:2 Changed 3 months ago by RyanGlScott

Thanks for the bug report. This is essentially a duplicate of #12088, which a long-standing issue in the way that groups of type-level declarations are kind-checked. #12088 itself has many other duplicates—last time I checked, these other tickets are also essentially duplicates of #12008:

One thing I did not realize before this ticket is that GHC's SCC analysis treats open and closed type families differently—thanks for that bit of knowledge! Another trick (that you may find useful) is that Template Haskell splices can often force the SCC analysis to come to its senses. For example, this variation on your program also compiles:

{-# LANGUAGE DataKinds       #-}
{-# LANGUAGE PolyKinds       #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies    #-}

module Bug where

import Data.Kind(Type)

type family FooKind (a :: Type) :: k
class Foo (a :: Type) where
  type FooType a :: FooKind a

-- OK
type instance FooKind Bool = Type
instance Foo Bool where
  type FooType Bool = Int

-- OK
data A
type instance FooKind A = Type
$(pure [])
instance Foo A where
  type FooType A = Int

It's a bit ugly, but it's a serviceable hack.

comment:3 Changed 3 months ago by sheaf

Thank you very much for that information Ryan. I can confirm that the Template Haskell hack has saved my biscuit. Sorry about the duplicate!

comment:4 Changed 3 months ago by RyanGlScott

Resolution: duplicate
Status: newclosed

No worries. To avoid having so many of these sorts of tickets floating around on Trac, I think I'll opt to close this one. If we do ever figure out a solution to #12088, though, we should make sure to add the program from this ticket as a test case, however. (I've added this ticket under the "related" field of #12088 to ensure that's more likely to happen.)

Note: See TracTickets for help on using tickets.