Some type families don't reduce with :kind!

changed weight to 5

I've managed to shrink it down to two modules, but unfortunately, I don't know how to trigger the issue without the use of cabal-install. I've put this minimal example at https://github.com/RyanGlScott/ghc-t11084, so you can reproduce the issue like so:

$ git clone https://github.com/RyanGlScott/ghc-t11084
$ cd ghc-t11084/
$ cabal install
$ ghci -XDataKinds
GHCi, version 8.4.2: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
λ> import T11084 
λ> :kind! Lookup 'True '[ '(True, True) ]
Lookup 'True '[ '(True, True) ] :: Maybe Bool
= T11084.Case
    'True 'True 'True '[] ('True ghc-t11084-0.1:PEq.== 'True)
λ> :kind! Lookup 'True '[ '(True, True) ]
Lookup 'True '[ '(True, True) ] :: Maybe Bool
= 'Just 'True

Here are the two modules in question:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module PEq where

type family (x :: a) == (y :: a) :: Bool
type instance a == b = EqBool a b

type family EqBool (a :: Bool) (b :: Bool) :: Bool where
  EqBool 'False      'False = 'True
  EqBool 'True       'True  = 'True
  EqBool _           _      = 'False

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module T11084 (Lookup) where

import PEq

type family Case key x y xys t where
  Case key x y xys 'True = 'Just y
  Case key x y xys 'False = Lookup key xys

type family Lookup (n :: a) (hs :: [(a, b)]) :: Maybe b where
  Lookup _key '[]             = 'Nothing
  Lookup key  ('(x, y) : xys) = Case key x y xys (key == x)

Some notes:

Having (==) and EqBool defined in a separate module from Lookup appears to be important. If you define them all in the same module, the bug no longer occurs.
Moreover, replacing (key == x) with EqBool key x in the definition of Lookup also makes the bug go away.

mentioned in issue #16234 (closed)

I've trimmed down this example even more:

{-# LANGUAGE TypeFamilies #-}
module T11084Aux where

type family F a
type instance F a = Int

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module T11084 where

import T11084Aux

type family G where
  G = F Char

Moreover, cabal new-build makes it much easier to reproduce this bug than it used to be. Now all you have to do is this:

$ git clone https://github.com/RyanGlScott/ghc-t11084
$ cd ghc-t11084/
$ cabal new-build -w /opt/ghc/8.6.3/bin/ghc --write-ghc-environment-files=always
$ /opt/ghc/8.6.3/bin/ghci -package-env .ghc.environment.x86_64-linux-8.6.3 
GHCi, version 8.6.3: http://www.haskell.org/ghc/  :? for help
Loaded package environment from .ghc.environment.x86_64-linux-8.6.3
Loaded package environment from .ghc.environment.x86_64-linux-8.6.3
Loaded GHCi configuration from /home/rgscott/.ghci
λ> import T11084 
λ> :kind! G
G :: *
= ghc-t11084-0.1:T11084Aux.F Char
λ> :kind! G
G :: *
= Int

added Pnormal label

mentioned in issue #16793 (closed)

mentioned in merge request !1377 (closed)

This bug is more general than just :kind!, as it affects :instances as well:

GHCi, version 8.11.0.20200120: https://www.haskell.org/ghc/  :? for help
Loaded package environment from /home/rgscott/Software/ghc-t11084/.ghc.environment.x86_64-linux-8.11.0.20200120
Loaded GHCi configuration from /home/rgscott/.ghci
λ> import T11084 
λ> :instances G
λ> :instances G
instance Eq Int -- Defined in ‘GHC.Classes’
instance Ord Int -- Defined in ‘GHC.Classes’
instance Enum Int -- Defined in ‘GHC.Enum’
instance Num Int -- Defined in ‘GHC.Num’
instance Real Int -- Defined in ‘GHC.Real’
instance Show Int -- Defined in ‘GHC.Show’
instance Read Int -- Defined in ‘GHC.Read’
instance Bounded Int -- Defined in ‘GHC.Enum’
instance Integral Int -- Defined in ‘GHC.Real’

(Not to be confused with #16793 (closed).)

I had originally suspected that this shares the same root cause as #16234 (closed). However, that appears not to be the case: #16234 (closed) no longer happens in GHC 9.6 or later, but this issue still persists as of GHC 9.10.1.

Trac field	Value
Version	7.10.2
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

Some type families don't reduce with :kind!

Child items 0

Activity