Opened 4 months ago

Closed 3 months ago

#15648 closed bug (fixed)

Core Lint error with source-level unboxed equality

Reported by: RyanGlScott Owned by:
Priority: normal Milestone: 8.8.1
Component: Compiler Version: 8.4.3
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Compile-time crash or panic Test Case:
Blocked By: Blocking:
Related Tickets: #15209 Differential Rev(s):
Wiki Page:

Description

I thought that we had killed (~#) from the source language in #15209. I could not have been more wrong. Source-level (~#) is alive and well, and it can cause Core Lint errors. Be afraid. Be very, very afraid.

The trick is to grab (~#) using Template Haskell:

module Foo where

import Language.Haskell.TH.Lib
import Language.Haskell.TH.Syntax

ueqT :: Q Type
ueqT = conT $ mkNameG_tc "ghc-prim" "GHC.Prim" "~#"

Once this is done, you can plop unboxed equality wherever you want into the source language. Here is a particularly mischievous example:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
module Bug where

import Data.Kind (Type)
import Data.Type.Equality (type (~~))
import Foo (ueqT)

data LegitEquality :: Type -> Type -> Type where
  Legit :: LegitEquality a a

data JankyEquality :: Type -> Type -> Type where
  Jank :: $ueqT a b -> JankyEquality a b

unJank :: JankyEquality a b -> $ueqT a b
unJank (Jank x) = x

legitToJank :: LegitEquality a b -> JankyEquality a b
legitToJank Legit = Jank

mkLegit :: a ~~ b => LegitEquality a b
mkLegit = Legit

ueqSym :: forall (a :: Type) (b :: Type).
          $ueqT a b -> $ueqT b a
ueqSym = unJank $ legitToJank $ mkLegit @b @a

If you compile this with optimizations, then GHC's inner demons are unleashed, which brings utter chaos when -dcore-lint is enabled:

$ /opt/ghc/8.6.1/bin/ghc -O2 -fforce-recomp Bug.hs -dcore-lint                           
[1 of 2] Compiling Foo              ( Foo.hs, Foo.o )
[2 of 2] Compiling Bug              ( Bug.hs, Bug.o )
*** Core Lint errors : in result of Simplifier ***
<no location info>: warning:
    [in body of lambda with binder co_a5RY :: a_a5RV ~# b_a5RW]
    x_a5OX :: b_a5RW ~# a_a5RV
    [LclId] is out of scope
*** Offending Program ***

<elided>

ueqSym :: forall a b. (a ~# b) => b ~# a
[LclIdX,
 Arity=1,
 Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
         WorkFree=True, Expandable=True,
         Guidance=ALWAYS_IF(arity=1,unsat_ok=True,boring_ok=True)}]
ueqSym
  = \ (@ a_a5RV) (@ b_a5RW) (co_a5RY :: a_a5RV ~# b_a5RW) -> x_a5OX

Obviously, this ticket is a little tongue-in-cheek, since I'm probably inviting disaster upon myself by deliberately digging around in ghc-prim for (~#). But this does raise the question: should we allow users to do this? I used to think that there was no harm in leaving (~#) lying at the bottom of the catacombs that is ghc-prim, but this example shows that perhaps (~#) should be locked away for good.

Change History (17)

comment:1 Changed 4 months ago by goldfire

Sigh.

I see two problems here:

  1. Why does GHC type check Jank at type JankyEquality a b? There must be something in the type checker which treats arguments of type a ~# b as invisible. But these shouldn't be -- they are not Constraints. To fix: find this code and kill it.
  1. What on earth was the simplifier thinking?!? To fix: find this code and encourage it to get an education.

I'd be less alarmed if the core lint error were right in the desugarer. Then, we could plausibly argue that forbidding ~# from source would fix the problem. But if the simplifier is doing it, there's got to be a legitimate bug (or, at least, a delicate invariant) somewhere.

I don't think we should be able to get a lint error just by writing ~# in the source.

comment:2 Changed 4 months ago by RyanGlScott

More shenanigans: if you put this at the end of Bug.hs:

main :: IO ()
main = case ueqSym @Bool @Bool of
         _ -> mkLegit `seq` print ()

Then you'll get an outright panic when you compile it:

$ /opt/ghc/8.6.1/bin/ghc -O2 -fforce-recomp Bug.hs
[1 of 2] Compiling Foo              ( Foo.hs, Foo.o )
[2 of 2] Compiling Bug              ( Bug.hs, Bug.o )
ghc: panic! (the 'impossible' happened)
  (GHC version 8.6.0.20180907 for x86_64-unknown-linux):
        StgCmmEnv: variable not found
  x_a5Pc
  local binds for:
  main
  $tc'Jank
  $trModule
  $tc'Jank2
  $tc'Jank1
  $tc'Jank3
  $tc'Legit
  $tc'Legit2
  $tc'Legit1
  $tc'Legit3
  $tcJankyEquality
  $tcJankyEquality1
  $tcJankyEquality2
  $tcLegitEquality
  $tcLegitEquality1
  $tcLegitEquality2
  $trModule3
  $trModule1
  $trModule2
  $trModule4
  main1
  $WLegit
  $krep_r6Fh
  $krep1_r6Fi
  $krep2_r6Fj
  $krep3_r6Fk
  $krep4_r6Fl
  $krep5_r6Fm
  $krep6_r6Fn
  $krep7_r6Fo
  $krep8_r6Fp
  $krep9_r6Fq
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
        pprPanic, called at compiler/codeGen/StgCmmEnv.hs:149:9 in ghc:StgCmmEnv

comment:3 Changed 4 months ago by goldfire

Did you have -dcore-lint on in comment:2? That looks like the lint error from above.

comment:4 in reply to:  3 Changed 4 months ago by RyanGlScott

Replying to goldfire:

Did you have -dcore-lint on in comment:2?

I didn't (it'll give the same Core Lint error as before if you do). I just wanted to give an example which shows that the problem is more severe than just an ordinary Core Lint warning (i.e., you can make GHC crash without needing to resort to debugging flags like -dcore-lint).

comment:5 in reply to:  1 Changed 4 months ago by RyanGlScott

Replying to goldfire:

  1. Why does GHC type check Jank at type JankyEquality a b? There must be something in the type checker which treats arguments of type a ~# b as invisible. But these shouldn't be -- they are not Constraints. To fix: find this code and kill it.

I think there is a simpler explanation for why this happens: when we kind-check the type (a ~# b) -> c, everything works since (->) is levity polymorphic and a ~# b has kind TYPE (TupleRep '[]). This means that resulting Type is FunTy (TyConApp (~#) [TyVarTy a, TyVarTy b]) (TyVarTy c)—which GHC believes to be (a ~# b) => c—so things like Jank are seemingly typechecked as if the value of type a ~# b were invisible.

From a certain perspective, this is a natural consequence of making a ~# b have kind TYPE (TupleRep '[]). This suggests that one way to work around this issue would be to change its kind.

comment:6 Changed 4 months ago by simonpj

I can see several things here.

  1. (~#) has a funny kind (see prelude/TysPrim:
    (~#) :: forall k1 k2. k1 -> k2 -> TYPE (TupleRep [])
    
    The kind TYPE TupleRep [] says that values of this type are represented by a zero-tuple of values; which takes zero bits.
  1. Note that it does not have return kind Constraint. Indeed, it can't, because that would mean it had a boxed, lifted representation, since (after the type checker) Constraint and Type are the same. So it won't behave like an invisible argument, because it doesn't have kind Constraint. Making (~#) behave like (~) in source code would be problematic for this reason.
  1. In Core, term-level variables (Id) are split into coercion variables (CoVars) and all others; distinguished by their IdDetails field, and isCoVarId. Coercion variables can be bound in terms (say by a lambda) but, unlike other Ids, can occur only in types and coercions. The simplifier keeps them in a different environment for that reason. In short:
  • A variable should reply True to isCoVarId iff it has type t1 ~# t2 or t1 ~R# t2.
  • A CoVar should occur only in types or coercions, never in a term (i.e. Var in Core).

Lint checks for the latter, but not the former; I'll fix that.

  1. This program has a non-CoVar bound by a lambda, and that's why the simplifier is breaking.

TL;DR: there a shortcoming in Lint, which I'll fix. Beyond that, GHC should really give a better error than a Lint failure in this case, but it's a bit exotic, and I'm not really sure where the best place to do it is. Maybe chekcValidType?

comment:7 Changed 4 months ago by goldfire

I worry a malicious user of TH might get around the checkValidType check.

Why do we need

  • If x :: t1 ~# t2, then x is a CoVar

? We clearly need the other direction of implication (that all CoVars have coercion types), but I don't see the harm in allowing non-CoVars to have coercion types. They'd be useless, but also harmless, I think.

I wonder if there is just some code that looks at an Id's type to determine whether it's a coercion variable instead of checking isCoVar. This might be from the fact that CoVar's distinguished nature in IdDetails is a relatively new innovation. It used to be that looking at the type was the only way to tell coercion variables from others.

comment:8 Changed 4 months ago by simonpj

Richard asks why this typechecks:

legitToJank :: LegitEquality a b -> JankyEquality a b
legitToJank Legit = Jank

given that

  Jank :: $ueqT a b -> JankyEquality a b

Turns it it's because tcSplitSigmaTy ultimately uses isPredTy to decide which the invisible arguments are. And isPredTy has a special case to return True for t1 ~# t2 and t1 ~R# t2.

I'm not sure of the consequences of making isPredTy return False for t1 ~# t2. (E.g. it is used in isEvVar.)

I'm a bit confused about what the Right Thing to do is.

comment:9 Changed 4 months ago by goldfire

isPredTy should almost certainly return False for t1 ~# t2. Code that wants to consider t1 ~# t2 alongside other predicates can use isPredTy ty || isConstraintType ty.

I think I made isPredTy recognize t1 ~# t2 during the -XTypeInType implementation, but I don't think it's necessary anymore.

comment:10 Changed 4 months ago by simonpj

isPredTy should almost certainly return False for t1 ~# t2.

That's a clear statement, and I think I agree -- but what argument(s) can you make to support that position. After all, t1 ~# t2 certainly is a constraint (predicate).

comment:11 Changed 4 months ago by goldfire

But it's not a constraint -- it's something else. Constraints are types of kind Constraint. Indeed, isPredTy should probably just check the kind.

comment:12 Changed 3 months ago by Simon Peyton Jones <simonpj@…>

In e7ff934/ghc:

Make Lint check that for CoVars more carefully

Check than an Id of type (t1 ~# t2) is a CoVar; if not,
it ends up in the wrong simplifier environment, with
strange consequences. (Trac #15648)

comment:13 Changed 3 months ago by Simon Peyton Jones <simonpj@…>

In 0faf7fd3/ghc:

Refactor the treatment of predicate types

Trac #15648 showed that GHC was a bit confused about the
difference between the types for

* Predicates
* Coercions
* Evidence (in the typechecker constraint solver)

This patch cleans it up. See especially Type.hs
Note [Types for coercions, predicates, and evidence]

Particular changes

* Coercion types (a ~# b) and (a ~#R b) are not predicate types
  (so isPredTy reports False for them) and are not implicitly
  instantiated by the type checker.  This is a real change, but
  it consistently reflects that fact that (~#) and (~R#) really
  are different from predicates.

* isCoercionType is renamed to isCoVarType

* During type inference, simplifyInfer, we do /not/ want to infer
  a constraint (a ~# b), because that is no longer a predicate type.
  So we 'lift' it to (a ~ b). See TcType
  Note [Lift equality constaints when quantifying]

* During type inference for pattern synonyms, we need to 'lift'
  provided constraints of type (a ~# b) to (a ~ b).  See
  Note [Equality evidence in pattern synonyms] in PatSyn

* But what about (forall a. Eq a => a ~# b)? Is that a
  predicate type?  No -- it does not have kind Constraint.
  Is it an evidence type?  Perhaps, but awkwardly so.

  In the end I decided NOT to make it an evidence type,
  and to ensure the the type inference engine never
  meets it.  This made me /simplify/ the code in
  TcCanonical.makeSuperClasses; see TcCanonical
  Note [Equality superclasses in quantified constraints]

  Instead I moved the special treatment for primitive
  equality to TcInteract.doTopReactOther.  See TcInteract
  Note [Looking up primitive equalities in quantified constraints]

  Also see Note [Evidence for quantified constraints] in Type.

  All this means I can have
     isEvVarType ty = isCoVarType ty || isPredTy ty
  which is nice.

All in all, rather a lot of work for a small refactoring,
but I think it's a real improvement.

comment:14 Changed 3 months ago by RyanGlScott

Good news—the original program is now rejected:

$ ~/Software/ghc/inplace/bin/ghc-stage2 Bug.hs[1 of 2] Compiling Foo              ( Foo.hs, Foo.o )
[2 of 2] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:23:21: error:
    • Couldn't match type ‘(a0 ~ b0) -> JankyEquality a0 b0’
                     with ‘JankyEquality a a’
      Expected type: JankyEquality a b
        Actual type: (a0 ~ b0) -> JankyEquality a0 b0
    • Probable cause: ‘Jank’ is applied to too few arguments
      In the expression: Jank
      In an equation for ‘legitToJank’: legitToJank Legit = Jank
    • Relevant bindings include
        legitToJank :: LegitEquality a b -> JankyEquality a b
          (bound at Bug.hs:23:1)
   |
23 | legitToJank Legit = Jank
   |                     ^^^^

Bug.hs:30:10: error:
    • Couldn't match expected type ‘(a ~ b) -> b ~ a’
                  with actual type ‘b ~ a’
    • In the expression: unJank $ legitToJank $ mkLegit @b @a
      In an equation for ‘ueqSym’:
          ueqSym = unJank $ legitToJank $ mkLegit @b @a
    • Relevant bindings include
        ueqSym :: (a ~ b) -> b ~ a (bound at Bug.hs:30:1)
   |
30 | ueqSym = unJank $ legitToJank $ mkLegit @b @a
   |          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

You can still use $ueqT a b as a visible argument to a function, but it appears to be functionally inert now, since you can't bring equalities into scope with it anymore (at least, not as far as I can tell).

Should we claim victory on this ticket?

comment:15 Changed 3 months ago by simonpj

I think so. I'm just about to add a test case.

comment:16 Changed 3 months ago by Simon Peyton Jones <simonpj@…>

In a3476aa2/ghc:

Test Trac #15648

comment:17 Changed 3 months ago by simonpj

Resolution: fixed
Status: newclosed
Note: See TracTickets for help on using tickets.