Opened 4 years ago

Last modified 8 months ago

#11084 new bug

Some type families don't reduce with :kind!

Reported by: goldfire Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.10.2
Keywords: TypeFamilies Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

Sadly, I'm unable to reproduce this without singletons. :(

Observe:

> ghci
GHCi, version 7.10.2: http://www.haskell.org/ghc/  :? for help
Prelude> import Data.Promotion.Prelude   -- singletons-2.0.1
Prelude Data.Promotion.Prelude> :kind! Lookup 'True '[ '(True, True) ]
Lookup 'True '[ '(True, True) ] :: Maybe Bool
= Data.Singletons.Prelude.List.Case_1628035408
    'True
    'True
    'True
    '[]
    (Data.Singletons.Apply (Data.Singletons.Apply (:==$) 'True) 'True)
Prelude Data.Promotion.Prelude> :kind! Lookup 'True '[ '(True, True) ]
Lookup 'True '[ '(True, True) ] :: Maybe Bool
= JustSym1 'True

Note that the exact same command run twice yields different results. I tried peeking at -ddump-tc-trace but got nothing of use.

Change History (3)

comment:1 Changed 4 years ago by thomie

Keywords: TypeFamilies added

comment:2 Changed 16 months ago by RyanGlScott

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:

  1. 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.
  2. Moreover, replacing (key == x) with EqBool key x in the definition of Lookup also makes the bug go away.

comment:3 Changed 8 months ago by RyanGlScott

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
$ /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
Note: See TracTickets for help on using tickets.