Re: [GHC] #11084: Some type families don't reduce with :kind!

18 May 2018

      #11084: Some type families don't reduce with :kind!
-------------------------------------+-------------------------------------
        Reporter:  goldfire          |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  7.10.2
      Resolution:                    |             Keywords:  TypeFamilies
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (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:

 {{{#!hs
 {-# 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
 }}}
 {{{#!hs
 {-# 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.

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11084#comment:2
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler