Opened 7 weeks ago

Last modified 7 weeks ago

#13790 new bug

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

Reported by: RyanGlScott Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 8.2.1-rc2
Keywords: TypeInType, TypeFamilies Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

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.

Change History (2)

comment:1 Changed 7 weeks ago by goldfire

Could this be a concrete example that tickles the problems discussed in #12088? Perhaps. Either that, or the fix for #11348 didn't go far enough.

comment:2 Changed 7 weeks ago by simonpj

To me it looks just lie #12088. To which I think we have a plan but it needs execution.

Note: See TracTickets for help on using tickets.