Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
GHC
GHC
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 4,323
    • Issues 4,323
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
    • Iterations
  • Merge Requests 372
    • Merge Requests 372
  • Requirements
    • Requirements
    • List
  • CI / CD
    • CI / CD
    • Pipelines
    • Jobs
    • Schedules
  • Security & Compliance
    • Security & Compliance
    • Dependency List
    • License Compliance
  • Operations
    • Operations
    • Incidents
    • Environments
  • Analytics
    • Analytics
    • CI / CD
    • Code Review
    • Insights
    • Issue
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Members
    • Members
  • Collapse sidebar
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
  • Glasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #15987

Closed
Open
Opened Dec 02, 2018 by sheaf@trac-sheafDeveloper

GHC sometimes not computing open type family application in kind inference

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.

Trac metadata
Trac field Value
Version 8.6.2
Type Bug
TypeOfFailure OtherFailure
Priority normal
Resolution Unresolved
Component Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture
Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking
None
Due date
None
Reference: ghc/ghc#15987