[GHC] #10488: Inconsistent reduction of type family

[GHC]

#10488: Inconsistent reduction of type family
-------------------------------------+-------------------------------------
              Reporter:  goldfire    |             Owner:
                  Type:  bug         |            Status:  new
              Priority:  highest     |         Milestone:  7.10.2
             Component:  Compiler    |           Version:  7.10.1
              Keywords:              |  Operating System:  Unknown/Multiple
          Architecture:              |   Type of failure:  None/Unknown
  Unknown/Multiple                   |        Blocked By:
             Test Case:              |   Related Tickets:
              Blocking:              |
Differential Revisions:              |
-------------------------------------+-------------------------------------
 Consider this module:

 {{{
 {-# LANGUAGE TemplateHaskell, TypeFamilies, GADTs, PolyKinds, DataKinds,
              ScopedTypeVariables, TypeOperators, UndecidableInstances #-}

 module SingBug where

 import Data.Singletons.TH

 $(promote [d|
   data Nat = Zero | Succ Nat
     deriving (Eq, Ord)
   |])

 foo :: Proxy (Zero :< Succ Zero)
 foo = (Proxy :: Proxy True)
 }}}

 It fails to compile, with this:

 {{{
 SingBug.hs:14:8:
     Couldn't match type ‘'False’ with ‘'True’
     Expected type: Proxy ('Zero :< 'Succ 'Zero)
       Actual type: Proxy 'True
     In the expression: (Proxy :: Proxy True)
     In an equation for ‘foo’: foo = (Proxy :: Proxy True)
 }}}

 However, if I remove the last two lines, it compiles fine. Witness this
 bizarre interaction:

 {{{
 Prelude> :load "SingBug.hs"
 [1 of 1] Compiling SingBug          ( SingBug.hs, interpreted )
 Ok, modules loaded: SingBug.
 *SingBug> :kind! Zero :< Succ Zero
 Zero :< Succ Zero :: Bool
 = TrueSym0
 *SingBug> :i TrueSym0
 type TrueSym0 = 'True
         -- Defined in ‘singletons-1.2:Data.Singletons.Prelude.Instances’
 *SingBug> :kind! (Proxy (Zero :< Succ Zero))
 (Proxy (Zero :< Succ Zero)) :: *
 = Proxy TrueSym0
 *SingBug> :t (Proxy :: Proxy (Zero :< Succ Zero))
 (Proxy :: Proxy (Zero :< Succ Zero))
   :: Proxy ('Zero :< 'Succ 'Zero)
 *SingBug> :t (Proxy :: Proxy (Zero :< Succ Zero)) :: Proxy True

 <interactive>:1:2:
     Couldn't match type ‘'False’ with ‘'True’
     Expected type: Proxy 'True
       Actual type: Proxy ('Zero :< 'Succ 'Zero)
     In the expression:
         (Proxy :: Proxy (Zero :< Succ Zero)) :: Proxy True
 *SingBug> :t (Proxy :: Proxy (Zero :< Succ Zero)) :: Proxy False
 (Proxy :: Proxy (Zero :< Succ Zero)) :: Proxy False :: Proxy 'False
 }}}

 It seems GHC can't decide if 0 is less than 1! When I ask it to use
 `:kind!`, it does the right thing. But if it's reducing a type during
 type-checking, it does very much the '''wrong''' thing.

 This is a regression compared to 7.8.

 I've been unable to minimize the test case or remove the `singletons`
 dependency, sadly. When I try to mimic the behavior of singletons without
 TH, it all works as expected.

 But I've found the problem. The apartness check for closed type families
 is very subtly broken, and I believe you can break the type system
 exploiting this bug. I can't quite tickle it directly though. Fix on the
 way in the next day.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/10488>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler