Opened 3 weeks ago
Last modified 64 minutes ago
#15346 merge bug
Core Lint error in GHC 8.6.1: Fromtype of Cast differs from type of enclosed expression
Reported by:  RyanGlScott  Owned by:  

Priority:  normal  Milestone:  8.6.1 
Component:  Compiler (Type checker)  Version:  8.5 
Keywords:  TypeInType  Cc:  
Operating System:  Unknown/Multiple  Architecture:  Unknown/Multiple 
Type of failure:  Compiletime crash or panic  Test Case:  dependent/should_compile/T15346 
Blocked By:  Blocking:  
Related Tickets:  #15419  Differential Rev(s):  
Wiki Page: 
Description
The following program typechecks on GHC 8.6.1alpha1:
{# LANGUAGE AllowAmbiguousTypes #} {# LANGUAGE DefaultSignatures #} {# LANGUAGE EmptyCase #} {# LANGUAGE FlexibleContexts #} {# LANGUAGE GADTs #} {# LANGUAGE ScopedTypeVariables #} {# LANGUAGE TypeFamilies #} {# LANGUAGE TypeInType #} {# LANGUAGE TypeOperators #} module SGenerics where import Data.Kind import Data.Type.Equality import Data.Void   singletons machinery  data family Sing :: forall k. k > Type data instance Sing :: () > Type where STuple0 :: Sing '() type Refuted a = a > Void data Decision a = Proved a  Disproved (Refuted a)   A stripped down version of GHC.Generics  data U1 = MkU1 data instance Sing (z :: U1) where SMkU1 :: Sing MkU1  class Generic (a :: Type) where type Rep a :: Type from :: a > Rep a to :: Rep a > a class PGeneric (a :: Type) where type PFrom (x :: a) :: Rep a type PTo (x :: Rep a) :: a class SGeneric k where sFrom :: forall (a :: k). Sing a > Sing (PFrom a) sTo :: forall (a :: Rep k). Sing a > Sing (PTo a :: k) sTof :: forall (a :: k). Sing a > PTo (PFrom a) :~: a sFot :: forall (a :: Rep k). Sing a > PFrom (PTo a :: k) :~: a  instance Generic () where type Rep () = U1 from () = MkU1 to MkU1 = () instance PGeneric () where type PFrom '() = MkU1 type PTo 'MkU1 = '() instance SGeneric () where sFrom STuple0 = SMkU1 sTo SMkU1 = STuple0 sTof STuple0 = Refl sFot SMkU1 = Refl  class SDecide k where   Compute a proof or disproof of equality, given two singletons. (%~) :: forall (a :: k) (b :: k). Sing a > Sing b > Decision (a :~: b) default (%~) :: forall (a :: k) (b :: k). (SGeneric k, SDecide (Rep k)) => Sing a > Sing b > Decision (a :~: b) s1 %~ s2 = case sFrom s1 %~ sFrom s2 of Proved (Refl :: PFrom a :~: PFrom b) > let r :: PTo (PFrom a) :~: PTo (PFrom b) r = Refl sTof1 :: PTo (PFrom a) :~: a sTof1 = sTof s1 sTof2 :: PTo (PFrom b) :~: b sTof2 = sTof s2 in Proved (sym sTof1 `trans` r `trans` sTof2) Disproved contra > Disproved (\Refl > contra Refl) instance SDecide U1 where SMkU1 %~ SMkU1 = Proved Refl instance SDecide ()
However, it throws a Core Lint error with dcorelint
. The full error is absolutely massive, so I'll attach it separately. Here is the toplevel bit:
*** Core Lint errors : in result of Simplifier *** <no location info>: warning: In the expression: <elided> Fromtype of Cast differs from type of enclosed expression Fromtype: U1 Type of enclosed expr: Rep () Actual enclosed expr: PFrom a_a1Fm Coercion used in cast: Sym (D:R:Rep()[0])
Attachments (1)
Change History (13)
Changed 3 weeks ago by
Attachment:  corelinterror.txt added 

comment:1 Changed 3 weeks ago by
That being said, Rep ()
should be equivalent to U1
, so I don't understand why the Core Lint error happens in the first place.
comment:2 Changed 3 weeks ago by
Here's a smaller version:
{# LANGUAGE AllowAmbiguousTypes #} {# LANGUAGE FlexibleContexts #} {# LANGUAGE ScopedTypeVariables #} {# LANGUAGE TypeFamilies #} {# LANGUAGE TypeInType #} {# LANGUAGE TypeApplications #} module SGenerics where import Data.Kind import Data.Proxy  type family Rep (a :: Type) :: Type type instance Rep () = () type family PFrom (x :: a) :: Rep a  class SDecide k where test :: forall (a :: k). Proxy a instance SDecide () where test = undefined test1 :: forall (a :: k). SDecide (Rep k) => Proxy a test1 = seq (test @_ @(PFrom a)) Proxy test2 :: forall (a :: ()). Proxy a test2 = test1
comment:3 Changed 2 weeks ago by
Thanks, monoidal. Your program also exhibits the same Core Lint error in GHC 8.4, unlike the original program.
I think it's actually easier to see what goes wrong if you add a second method to SDecide
so that there's not as many coercions cluttering up the dcorelint
output:
{# LANGUAGE AllowAmbiguousTypes #} {# LANGUAGE FlexibleContexts #} {# LANGUAGE ScopedTypeVariables #} {# LANGUAGE TypeFamilies #} {# LANGUAGE TypeInType #} {# LANGUAGE TypeApplications #} module SGenerics where import Data.Kind import Data.Proxy  type family Rep (a :: Type) :: Type type instance Rep () = () type family PFrom (x :: a) :: Rep a  class SDecide k where test :: forall (a :: k). Proxy a dummy :: k instance SDecide () where test = undefined dummy = undefined test1 :: forall (a :: k). SDecide (Rep k) => Proxy a test1 = seq (test @_ @(PFrom a)) Proxy test2 :: forall (a :: ()). Proxy a test2 = test1
$ /opt/ghc/8.6.1/bin/ghci Bug.hs dcorelint ddumptc <elided> [1 of 1] Compiling SGenerics ( Bug.hs, interpreted ) TYPE SIGNATURES dummy :: forall k. SDecide k => k test :: forall k (a :: k). SDecide k => Proxy a test1 :: forall k (a :: k). SDecide (Rep k) => Proxy a test2 :: forall (a :: ()). Proxy a TYPE CONSTRUCTORS type family PFrom (x :: a) :: Rep a open type family Rep a :: * open class SDecide k where test :: forall (a :: k). Proxy a dummy :: k {# MINIMAL test, dummy #} COERCION AXIOMS axiom SGenerics.D:R:Rep() :: Rep () = ()  Defined at Bug.hs:15:15 INSTANCES instance SDecide ()  Defined at Bug.hs:25:10 FAMILY INSTANCES type instance Rep () Dependent modules: [] Dependent packages: [base4.12.0.0, ghcprim0.5.3, integergmp1.0.2.0] ==================== Typechecker ==================== <elided> *** Core Lint errors : in result of Simplifier *** Bug.hs:32:1: warning: [in body of lambda with binder a_a1UE :: ()] Kind application error in coercion ‘(Proxy (Sym (D:R:Rep()[0])) <a_a1Dx>_P)_R’ Function kind = forall k. k > * Arg kinds = [(Rep (), *), (a_a1Dx, ())] Fun: Rep () (a_a1Dx, ()) Bug.hs:32:1: warning: [in body of lambda with binder a_a1UE :: ()] Fromtype of Cast differs from type of enclosed expression Fromtype: () Type of enclosed expr: Rep () Actual enclosed expr: PFrom a_a1UE Coercion used in cast: Sym (D:R:Rep()[0]) *** Offending Program *** <elided> test2 :: forall (a :: ()). Proxy a [LclIdX, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=False, ConLike=False, WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 10 10}] test2 = \ (@ (a_a1UE :: ())) > break<1>() break<0>() case ($ctest_a1UM @ (PFrom a_a1UE > D:R:Rep()[0])) `cast` (Inst (forall (a :: Sym (D:R:Rep()[0])). (Proxy (Sym (D:R:Rep()[0])) <a>_P)_R) (Coh <PFrom a_a1UE>_N (Sym (D:R:Rep()[0]))) :: Proxy (PFrom a_a1UE > Sym (D:R:Rep()[0])) ~R# Proxy (PFrom a_a1UE > D:R:Rep()[0])) of { Proxy > Proxy @ () @ a_a1UE }
Here, we can see exactly what goes wrong:
 In the definition of
test2
, we have the casted typeProxy (PFrom a_a1UE > Sym (D:R:Rep()[0]))
, wherea_a1UE :: ()
.  As can be seen in the
ddumptc
output,D:R:Rep()[0] :: Rep () ~# ()
. Therefore,Sym (D:R:Rep()[0]) :: () ~# Rep ()
.  However,
PFrom a_a1UE :: Rep ()
, so the coercionSym (D:R:Rep()[0])
is oriented the wrong way!
There's another tiny buglet here in that Core Lint is calling PFrom a_a1UE
an exclosed "expression", but it's actually a type. This is probably worth fixing separately.
comment:4 Changed 2 weeks ago by
Phab:D4940 changes the Core Lint error for kind coercions, as suggested in the bottom of comment:3.
comment:6 Changed 2 weeks ago by
I've had quite an adventure debugging this one. I haven't quite fixed everything, but I have discovered one surprising fact: GHC incorrectly implements the S_TPush
rule from System FC with Explicit Kind Equality. In particular, we have:
Γ ⊢_co γ : ∀ a: κ_1. σ_1 ~ ∀ a: κ_2. σ_2 γ' = sym (nth^1 γ) τ' = τ ⊳ γ'  S_TPush (ν ⊳ γ) τ > (ν τ') ⊳ γ@(<τ> ⊳ γ')
But in CoreOpt
, GHC implements this rule as:
pushCoTyArg :: CoercionR > Type > Maybe (Type, MCoercionR) pushCoTyArg co ty ...  isForAllTy tyL = ASSERT2( isForAllTy tyR, ppr co $$ ppr ty ) Just (ty `mkCastTy` mkSymCo co1, MCo co2) ... where Pair tyL tyR = coercionKind co  co :: tyL ~ tyR  tyL = forall (a1 :: k1). ty1  tyR = forall (a2 :: k2). ty2 co1 = mkNthCo Nominal 0 co  co1 :: k1 ~N k2 co2 = mkInstCo co (mkCoherenceLeftCo (mkNomReflCo ty) co1)  co2 :: ty1[ (ty>co1)/a1 ] ~ ty2[ ty/a2 ]
Here, co2
is supposed to correspond to γ@(<τ> ⊳ γ')
, or equivalently, γ@(<τ> ⊳ sym (nth^1 γ))
. But note that this definition isn't correct: co2
actually calculates γ@(<τ> ⊳ nth^1 γ)
, not γ@(<τ> ⊳ sym (nth^1 γ))
! To fix this, all one needs to do is apply this patch:

compiler/coreSyn/CoreOpt.hs
diff git a/compiler/coreSyn/CoreOpt.hs b/compiler/coreSyn/CoreOpt.hs index 0353ab6..5e37fee 100644
a b pushCoTyArg co ty 979 979 980 980  isForAllTy tyL 981 981 = ASSERT2( isForAllTy tyR, ppr co $$ ppr ty ) 982 Just (ty `mkCastTy` mkSymCoco1, MCo co2)982 Just (ty `mkCastTy` co1, MCo co2) 983 983 984 984  otherwise 985 985 = Nothing … … pushCoTyArg co ty 989 989  tyL = forall (a1 :: k1). ty1 990 990  tyR = forall (a2 :: k2). ty2 991 991 992 co1 = mk NthCo Nominal 0 co993  co1 :: k 1 ~N k2992 co1 = mkSymCo (mkNthCo Nominal 0 co) 993  co1 :: k2 ~N k1 994 994  Note that NthCo can extract a Nominal equality between the 995 995  kinds of the types related by a coercion between foralltypes. 996 996  See the NthCo case in CoreLint.
That fixes one of the Core Lint errors in comment:3, which is nice. But one remains even after applying that patch:
*** Core Lint errors : in result of Simplifier *** Bug.hs:32:1: warning: [in body of lambda with binder a_a1qX :: ()] Kind application error in coercion ‘(Proxy (Sym (D:R:Rep()[0])) <a_avO>_P)_R’ Function kind = forall k. k > Type Arg kinds = [(Rep (), Type), (a_avO, ())] Fun: Rep () (a_avO, ())
It appears that we shouldn't be constructing the coercion (Proxy (Sym (D:R:Rep()[0])) <a_avO>_P)_R
, as it's ill kinded. Using ddumprulerewrites
, we can see that this coercion is generated here:
Rule fired Rule: Class op test Module: (BUILTIN) Before: SGenerics.test TyArg SGenerics.Rep () ValArg SGenerics.$fSDecide() `cast` ((SGenerics.SDecide (Sym (SGenerics.D:R:Rep()[0])))_R :: SGenerics.SDecide () ~R# SGenerics.SDecide (SGenerics.Rep ())) After: $ctest_a1r5 `cast` (forall (a :: Sym (SGenerics.D:R:Rep()[0])). (Data.Proxy.Proxy (Sym (SGenerics.D:R:Rep()[0])) <a>_P)_R :: (forall (a :: ()). Data.Proxy.Proxy a) ~R# (forall (a :: SGenerics.Rep ()). Data.Proxy.Proxy (a > SGenerics.D:R:Rep()[0]))) Cont: ApplyToTy (SGenerics.PFrom a_a1qX) Select nodup wild_Xj Stop[RhsCtxt] Data.Proxy.Proxy a_a1qX
That's as far as I've come debugging thus far.
comment:7 Changed 2 weeks ago by
Wow. Good sleuthing. Yes, you're right about TPush. I'm boggled that we've gotten this far with that mistake in there. I may have time tomorrow to continue.
comment:8 Changed 2 weeks ago by
As far as the other Core Lint error goes, I think I've narrowed it down to pushCoDataCon (which implements the S_KPush
rule from System FC with Explicit Kind Equality), as that's the function that annotates $ctest
with the coercion forall (a :: Sym (D:R:Rep()[0])). (Proxy (Sym (D:R:Rep()[0])) <a>_P)_R
.
I tried tracing through the steps of S_KPush
to see if this coercion is what should have been produced, but I'm uncertain in my results simply because the way that GHC represents type abstraction congruence coercions is slightly different than the way they're represented in the paper.
In the paper, a type abstraction congruence coercion is of the form:
∀_η (a_1, a_2, c). γ
Where η
is a kind coercion, a_1
and a_2
are two fresh type variables inhabiting the from and tokinds of η
, respectively, and c
is a fresh coercion variable witnessing a_1 ~ a_2
. See the CT_AllT
rule in Figure 4 for a complete presentation of how it's typed.
Since the type of $ctest
is ∀(a : k). Proxy k a
, applying Ψ
to this type (where Ψ
is defined in Section 5 of the paper) should produce:
∀_(Sym (D:R:Rep()[0])) (a_1, a_2, c). <Proxy> (Sym (D:R:Rep()[0])) c
This does look a bit different than the coercion that GHC is actually producing, since the last argument to <Proxy>
is c
instead of <a>
. However, it's quite hard for me to determine if this difference is intentional, especially after reading GHC's Note [Forall coercions], which presents the typing rule as:
kind_co : k1 ~ k2 tv1:k1  co : t1 ~ t2  ForAllCo tv1 kind_co co : all tv1:k1. t1 ~ all tv1:k2. (t2[tv1 > tv1 > sym kind_co])
This presentation is quite different from the CT_AllT
typing rule in the paper, as it does not introduce two fresh type variables of different kinds equated by a coercion variable. Instead, it uses the same type variable in both sides of the ForAllCo
, and tries to fix up the kind of the type variable in the totype with this strange tv1 > sym kind_co
coercion.
GHC's unusual treatment of this typing rule at least explains why the kind of the coercion we see in this program is (forall (a :: ()). Proxy () a) ~R# (forall (a :: Rep ()). Proxy (Rep ()) (a > D:R:Rep()[0]))
. Still, I find it difficult to convince myself that this alternate treatment is correct. After all, the type forall (a :: Rep ()). Proxy (Rep ()) (a > D:R:Rep()[0])
looks blatantly ill kinded to me, since (a > D:R:Rep()[0])
is of kind ()
, not Rep ()
as it claims.
Richard, do you have any insights here?
comment:10 Changed 4 days ago by
Related Tickets:  → #15419 

I believe #15419 is a symptom of this bug.
comment:12 Changed 64 minutes ago by
Status:  new → merge 

Test Case:  → dependent/should_compile/T15346 
This should be merged  it's a downright bug with a tiny patch. Thanks.
dcorelint error output