[GHC] #10488: Inconsistent reduction of type family
GHC
ghc-devs at haskell.org
Thu Jun 4 21:03:29 UTC 2015
#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
More information about the ghc-tickets
mailing list