Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
  • GHC GHC
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 5,252
    • Issues 5,252
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 561
    • Merge requests 561
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
    • Test Cases
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Code review
    • Insights
    • Issue
    • Repository
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Glasgow Haskell CompilerGlasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #13790
Closed
Open
Issue created Jun 05, 2017 by Ryan Scott@RyanGlScottMaintainer

GHC doesn't reduce type family in kind signature unless its arm is twisted

Here's some code (inspired by Richard's musings here) which typechecks with GHC 8.2.1 or HEAD:

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

import Data.Kind

data family Sing (a :: k)

data SomeSing (k :: Type) where
  SomeSing :: Sing (a :: k) -> SomeSing k

type family Promote k :: Type

class (Promote (Demote k) ~ k) => SingKind (k :: Type) where
  type Demote k :: Type
  fromSing :: Sing (a :: k) -> Demote k
  toSing :: Demote k -> SomeSing k

type family DemoteX (a :: k) :: Demote k
type instance DemoteX (a :: Type) = Demote a

type instance Promote Type = Type

instance SingKind Type where
  type Demote Type = Type
  fromSing = error "fromSing Type"
  toSing   = error "toSing Type"

-----

data N = Z | S N

data instance Sing (z :: N) where
  SZ :: Sing Z
  SS :: Sing n -> Sing (S n)
type instance Promote N = N

instance SingKind N where
  type Demote N = N
  fromSing SZ = Z
  fromSing (SS n) = S (fromSing n)
  toSing Z = SomeSing SZ
  toSing (S n) = case toSing n of
                   SomeSing sn -> SomeSing (SS sn)

Things get more interesting if you try to add this type instance at the end of this file:

type instance DemoteX (n :: N) = n

Now GHC will complain:

GHCi, version 8.2.0.20170522: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )

Bug.hs:49:34: error:
    • Expected kind ‘Demote N’, but ‘n’ has kind ‘N’
    • In the type ‘n’
      In the type instance declaration for ‘DemoteX’
   |
49 | type instance DemoteX (n :: N) = n
   |                                  ^

That error message smells funny, since we do have a type family instance that says Demote N = N! In fact, if you use Template Haskell to split up the declarations manually:

...

instance SingKind N where
  type Demote N = N
  fromSing SZ = Z
  fromSing (SS n) = S (fromSing n)
  toSing Z = SomeSing SZ
  toSing (S n) = case toSing n of
                   SomeSing sn -> SomeSing (SS sn)
$(return [])
type instance DemoteX (n :: N) = n

Then the file typechecks without issue.

Trac metadata
Trac field Value
Version 8.2.1-rc2
Type Bug
TypeOfFailure OtherFailure
Priority normal
Resolution Unresolved
Component Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking