Opened 3 weeks ago

Last modified 64 minutes ago

#15346 merge bug

Core Lint error in GHC 8.6.1: From-type 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: Compile-time 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.1-alpha1:

{-# 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 -dcore-lint. The full error is absolutely massive, so I'll attach it separately. Here is the top-level bit:

*** Core Lint errors : in result of Simplifier ***
<no location info>: warning:
    In the expression: <elided>
    From-type of Cast differs from type of enclosed expression
    From-type: U1
    Type of enclosed expr: Rep ()
    Actual enclosed expr: PFrom a_a1Fm
    Coercion used in cast: Sym (D:R:Rep()[0])

Attachments (1)

core-lint-error.txt (113.7 KB) - added by RyanGlScott 3 weeks ago.
-dcore-lint error output

Download all attachments as: .zip

Change History (13)

Changed 3 weeks ago by RyanGlScott

Attachment: core-lint-error.txt added

-dcore-lint error output

comment:1 Changed 3 weeks ago by RyanGlScott

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 monoidal

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 RyanGlScott

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 -dcore-lint 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 -dcore-lint -ddump-tc
<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: [base-4.12.0.0, ghc-prim-0.5.3,
                     integer-gmp-1.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 :: ()]
    From-type of Cast differs from type of enclosed expression
    From-type: ()
    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 type Proxy (PFrom a_a1UE |> Sym (D:R:Rep()[0])), where a_a1UE :: ().
  • As can be seen in the -ddump-tc output, D:R:Rep()[0] :: Rep () ~# (). Therefore, Sym (D:R:Rep()[0]) :: () ~# Rep ().
  • However, PFrom a_a1UE :: Rep (), so the coercion Sym (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.

Last edited 2 weeks ago by RyanGlScott (previous) (diff)

comment:4 Changed 2 weeks ago by RyanGlScott

Phab:D4940 changes the Core Lint error for kind coercions, as suggested in the bottom of comment:3.

comment:5 Changed 2 weeks ago by Ryan Scott <ryan.gl.scott@…>

In 18cedbb5/ghc:

Make a variant of mkCastErr for kind coercions

Summary:
I discovered when debugging #15346 that the Core Lint error
message for ill typed casts always mentions types of enclosed
//expressions//, even if the thing being casted is actually a type.
This generalizes `mkCastErr` a bit to allow it to give the proper
labelling for kind coercions.

Test Plan: Run on failing program in #15346, read the Core Lint error

Reviewers: goldfire, bgamari, simonpj

Reviewed By: simonpj

Subscribers: simonpj, rwbarton, thomie, carter

Differential Revision: https://phabricator.haskell.org/D4940

comment:6 Changed 2 weeks ago by RyanGlScott

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 
    979979
    980980  | isForAllTy tyL
    981981  = ASSERT2( isForAllTy tyR, ppr co $$ ppr ty )
    982     Just (ty `mkCastTy` mkSymCo co1, MCo co2)
     982    Just (ty `mkCastTy` co1, MCo co2)
    983983
    984984  | otherwise
    985985  = Nothing
    pushCoTyArg co ty 
    989989       -- tyL = forall (a1 :: k1). ty1
    990990       -- tyR = forall (a2 :: k2). ty2
    991991
    992     co1 = mkNthCo Nominal 0 co
    993        -- co1 :: k1 ~N k2
     992    co1 = mkSymCo (mkNthCo Nominal 0 co)
     993       -- co1 :: k2 ~N k1
    994994       -- Note that NthCo can extract a Nominal equality between the
    995995       -- kinds of the types related by a coercion between forall-types.
    996996       -- 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 -ddump-rule-rewrites, 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.

Last edited 2 weeks ago by RyanGlScott (previous) (diff)

comment:7 Changed 2 weeks ago by goldfire

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 RyanGlScott

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 to-kinds 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 to-type 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:9 Changed 2 weeks ago by Ryan Scott <ryan.gl.scott@…>

In 6595bee/ghc:

Define an Outputable MCoercion instance

Summary: I needed this when debugging #15346.

Test Plan: Does it compile? It does? Cool.

Reviewers: bgamari, mpickering

Reviewed By: mpickering

Subscribers: rwbarton, thomie, carter

GHC Trac Issues: #15311

Differential Revision: https://phabricator.haskell.org/D4944

comment:10 Changed 4 days ago by RyanGlScott

I believe #15419 is a symptom of this bug.

comment:11 Changed 65 minutes ago by Richard Eisenberg <rae@…>

In af624071/ghc:

Fix some casts.

This fixes #15346, and is a team effort between Ryan Scott and
myself (mostly Ryan). We discovered two errors related to FC's
"push" rules, one in the TPush rule (as implemented in pushCoTyArg)
and one in KPush rule (it shows up in liftCoSubstVarBndr).

The solution: do what the paper says, instead of whatever random
thoughts popped into my head as I was actually implementing.

Also fixes #15419, which is actually the same underlying problem.

Test case: dependent/should_compile/T{15346,15419}.

comment:12 Changed 64 minutes ago by goldfire

Status: newmerge
Test Case: dependent/should_compile/T15346

This should be merged -- it's a downright bug with a tiny patch. Thanks.

Note: See TracTickets for help on using tickets.