Inconsistent reduction of type family

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.

Trac metadata

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