[GHC] #15987: GHC sometimes not computing open type family application in kind inference

2 Dec 2018

      #15987: GHC sometimes not computing open type family application in kind inference
-------------------------------------+-------------------------------------
           Reporter:  sheaf          |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.6.2
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  GHC rejects
  Unknown/Multiple                   |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 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:

 {{{#!hs
 {-# 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:
 {{{#!hs
 (     (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.

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15987
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler

GHC

GHC

GHC

GHC

GHC

tags

participants (1)