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 |