Type family recklessly concludes apartness, causing unsoundness
(Spun off from #9 (comment 215910).) You can implement unsafeCoerce
with a devious use of type families:
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UnsaturatedTypeFamilies #-}
module Bug where
import Data.Kind
import Data.Type.Equality
type family IfEq a b t f where
IfEq a a t _ = t
IfEq a b _ f = f
type Const a b = a
type Id a = a
ohNo :: forall (f :: Type ~> Type) (g :: Type ~> Type) a b c d.
IfEq (f c) (f d) a b -> IfEq (g c) (g d) a b
ohNo = id
unsafeCoerce :: forall a b. a -> b
unsafeCoerce = ohNo @(Const Char) @Id @a @b @Int @Bool
Note that this will produce the following Core Lint error:
$ ~/Software/ghc-kcsongor/inplace/bin/ghc-stage2 Bug.hs -dcore-lint
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
*** Core Lint errors : in result of Simplifier ***
Bug.hs:22:1: warning:
[RHS of unsafeCoerce :: forall a b. a ~> b]
Bad axiom application (inconsistent with IfEq a a t _ = t_awT
-- Defined at Bug.hs:11:3)
D:R:IfEq[1]
<Const Char Int>_N <Const Char Bool>_N <a_a145>_N <b_a146>_N
*** Offending Program ***
ohNo
:: forall (f :: * ~> *) (g :: * ~> *) a b c d.
IfEq (f c) (f d) a b ~> IfEq (g c) (g d) a b
[LclIdX,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=False, ConLike=False,
WorkFree=True, Expandable=True,
Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=True)}]
ohNo
= (\ (@ (f_a13T :: * ~> *))
(@ (g_a13U :: * ~> *))
(@ a_a13V)
(@ b_a13W)
(@ c_a13X)
(@ d_a13Y) ->
id @ b_a13W)
`cast` (forall (f :: <* ~> *>_N) (g :: <*
~> *>_N) (a :: <*>_N) (b :: <*>_N) (c :: <*>_N) (d :: <*>_N).
Sub (Sym (D:R:IfEq[1] <f c>_N <f d>_N <a>_N <b>_N))
->{<'Unmatchable>_N}_R Sub (Sym (D:R:IfEq[1]
<g c>_N <g d>_N <a>_N <b>_N))
:: (forall (f :: * ~> *) (g :: * ~> *) a b c d. b ~> b)
~R# (forall (f :: * ~> *) (g :: * ~> *) a b c d.
IfEq (f c) (f d) a b ~> IfEq (g c) (g d) a b))
unsafeCoerce :: forall a b. a ~> b
[LclIdX,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=False, ConLike=False,
WorkFree=True, Expandable=True,
Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=True)}]
unsafeCoerce
= (\ (@ a_a145) (@ b_a146) -> id @ b_a146)
`cast` (forall (a :: <*>_N) (b :: <*>_N).
(Sub (Sym (D:R:IfEq[1]
<Const Char Int>_N <Const Char Bool>_N <a>_N <b>_N))
->{<'Unmatchable>_N}_R Sub (Sym (D:R:IfEq[1]
<Id Int>_N
<Id Bool>_N
<a>_N
<b>_N))) ; (Sub (D:R:IfEq[0] <Char>_N <a>_N <b>_N)
->{<'Unmatchable>_N}_R Sub (D:R:IfEq[1]
<Int>_N
<Bool>_N
<a>_N
<b>_N))
:: (forall a b. b ~> b) ~R# (forall a b. a ~> b))
$trModule_s1g2 :: Addr#
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 20 0}]
$trModule_s1g2 = "main"#
$trModule_s1g3 :: TrName
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 20}]
$trModule_s1g3 = TrNameS $trModule_s1g2
$trModule_s1g4 :: Addr#
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 20 0}]
$trModule_s1g4 = "Bug"#
$trModule_s1g5 :: TrName
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 20}]
$trModule_s1g5 = TrNameS $trModule_s1g4
$trModule :: Module
[LclIdX,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 30}]
$trModule = Module $trModule_s1g3 $trModule_s1g5
*** End of Offense ***
<no location info>: error:
Compilation had errors
The root of the problem appears to be that GHC concludes that f a
and f b
are apart for all f
, a
, and b
:
λ> :kind! forall (f :: Type ~> Type) a b. IfEq (f a) (f b) Int Bool
forall (f :: Type ~> Type) a b. IfEq (f a) (f b) Int Bool :: *
= Bool