Opened 15 months ago

Last modified 13 months ago

#15552 merge bug

Infinite loop/panic with an existential type.

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

Description

The symptoms of this bug are quite similar to #14723, but I don't know if the cause is exactly the same, ergo a new report.

To reproduce:

  1. Make T.hs
    {-# LANGUAGE DataKinds, ExistentialQuantification, GADTs, PolyKinds, TypeOperators #-}
    module T where
    
    import Data.Kind
    
    data Elem :: k -> [k] -> Type where
      Here :: Elem x (x : xs)
      There :: Elem x xs -> Elem x (y : xs)
    
    data EntryOfVal (v :: Type) (kvs :: [Type]) = forall (k :: Type). EntryOfVal (Elem (k, v) kvs)
    
  1. Compile it with ghc T.hs -ddump-tc-trace
    # etc.
    checkExpectedKind
      *
      TYPE t_aXd[tau:1]
      <*>_N
    kcLHsQTyVars: not-cusk
      EntryOfVal
      []
      [(k_aW0 :: Type)]
      []
      [k_aW0[sk:1]]
      *ghc: panic! (the 'impossible' happened)
      (GHC version 8.4.3 for x86_64-apple-darwin):
    	kcConDecl
    
    Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug
    
  1. Append the following to T.hs (not minimized, sorry)
    type family EntryOfValKey (eov :: EntryOfVal v kvs) :: Type where
      EntryOfValKey ('EntryOfVal (_ :: Elem (k, v) kvs)) = k
    type family GetEntryOfVal (eov :: EntryOfVal v kvs) :: Elem (EntryOfValKey eov, v) kvs where
      GetEntryOfVal ('EntryOfVal e) = e
    
    type family FirstEntryOfVal (v :: Type) (kvs :: [Type]) :: EntryOfVal v kvs where
      FirstEntryOfVal v ((k, v) : _) = 'EntryOfVal Here
      FirstEntryOfVal v (_ : kvs) = 'EntryOfVal (There (GetEntryOfVal (FirstEntryOfVal v kvs)))
    
  1. Compile with a plain ghc T.hs
    1. Wait until bored, then knock the compiler out of its infinite loop by killing it.
  2. Compile again with ghc T.hs -ddump-tc-trace
    # etc.
    checkExpectedKind
      *
      TYPE t_aYg[tau:1]
      <*>_N
    kcLHsQTyVars: not-cuskghc: panic! (the 'impossible' happened)
      (GHC version 8.4.3 for x86_64-apple-darwin):
    	kcConDecl
    
    Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug
    

Found while trying to answer this SO question.

Change History (13)

comment:1 Changed 15 months ago by RyanGlScott

Keywords: TypeInType TypeFamilies added

The -ddump-tc-trace panic is an old GHC 8.4.3 bug that has since been fixed. (I can't recall if there was ever a ticket to track this.)

I wasn't able to reproduce the infinite loop until I added some more language extensions (TypeInType and TypeFamilies):

{-# LANGUAGE DataKinds, ExistentialQuantification, GADTs, PolyKinds, TypeOperators #-}
{-# LANGUAGE TypeInType, TypeFamilies #-}
module T where

import Data.Kind

data Elem :: k -> [k] -> Type where
  Here :: Elem x (x : xs)
  There :: Elem x xs -> Elem x (y : xs)

data EntryOfVal (v :: Type) (kvs :: [Type]) = forall (k :: Type). EntryOfVal (Elem (k, v) kvs)

type family EntryOfValKey (eov :: EntryOfVal v kvs) :: Type where
  EntryOfValKey ('EntryOfVal (_ :: Elem (k, v) kvs)) = k
type family GetEntryOfVal (eov :: EntryOfVal v kvs) :: Elem (EntryOfValKey eov, v) kvs where
  GetEntryOfVal ('EntryOfVal e) = e

type family FirstEntryOfVal (v :: Type) (kvs :: [Type]) :: EntryOfVal v kvs where
  FirstEntryOfVal v ((k, v) : _) = 'EntryOfVal Here
  FirstEntryOfVal v (_ : kvs) = 'EntryOfVal (There (GetEntryOfVal (FirstEntryOfVal v kvs)))

This still loops when compiled even on 8.6 and HEAD. I wonder if there is any relationship between this ticket and #15473...

comment:2 Changed 15 months ago by simonpj

It's not #15473. Something to do with zonking the type in tcyFamInstEqn

tcTyFamInstEqn fam_tc mb_clsinfo
    (L loc (HsIB { hsib_ext = tv_names
                 , hsib_body = FamEqn { feqn_tycon  = L _ eqn_tc_name
                                      , feqn_pats   = pats
                                      , feqn_rhs    = hs_ty }}))
  = ASSERT( getName fam_tc == eqn_tc_name )
    setSrcSpan loc $
    tcFamTyPats fam_tc mb_clsinfo tv_names pats
                (kcTyFamEqnRhs mb_clsinfo hs_ty) $
                    \tvs pats res_kind ->
    do { traceTc "tcTyFamInstEqn {" (ppr eqn_tc_name <+> ppr pats)
       ; rhs_ty <- solveEqualities $ tcCheckLHsType hs_ty res_kind
       ; traceTc "tcTyFamInstEqn 1" (ppr eqn_tc_name <+> ppr pats)
       ; (ze, tvs') <- zonkTyBndrsX emptyZonkEnv tvs
       ; traceTc "tcTyFamInstEqn 2" (ppr eqn_tc_name <+> ppr pats)
       ; pats'      <- zonkTcTypeToTypes ze pats
       ; traceTc "tcTyFamInstEqn 3" (ppr eqn_tc_name <+> ppr pats $$ ppr rhs_ty)
       ; rhs_ty'    <- zonkTcTypeToType ze rhs_ty
       ; traceTc "tcTyFamInstEqn 4" (ppr fam_tc <+> pprTyVars tvs')
       ; return (mkCoAxBranch tvs' [] pats' rhs_ty'

We get to "3" but not to "4".

comment:3 Changed 15 months ago by simonpj

OK I finally understand what is going on.

Suppose we have

alpha -> alpha
where
  alpha is already unified:
    alpha := T{tc-tycon} Int -> Int
  and T is knot-tied

By "knot-tied" I mean that the occurrence of T is currently a TcTyCon, but the global env contains a mapping "T" :-> T{knot-tied-tc}. See Note [Type checking recursive type and class declarations] in TcTyClsDecls.

Now we call zonkTcTypeToType on that alpha -> alpha.

  • The first time we encounter alpha we invoke TcHsTyn.zonkTyVarOcc (because that's what the tcm_tyvar field of zonk_tycomapper says. Here's the code
    zonkTyVarOcc env@(ZonkEnv zonk_unbound_tyvar tv_env _) tv
      | isTcTyVar tv
      = case tcTyVarDetails tv of
             SkolemTv {}    -> lookup_in_env
             RuntimeUnk {}  -> lookup_in_env
             MetaTv { mtv_ref = ref }
               -> do { cts <- readMutVar ref
                     ; case cts of
                          Flexi -> do { kind <- zonkTcTypeToType env (tyVarKind tv)
                                      ; zonk_unbound_tyvar (setTyVarKind tv kind) }
                          Indirect ty -> do { zty <- zonkTcTypeToType env ty
                                            -- Small optimisation: shortern-out indirect steps
                                            -- so that the old type may be more easily collected.
                                            ; writeMutVar ref (Indirect zty)
                                            ; return zty } }
    
  • zonkTyVarOcc sees that the tyvar is already unifies (the Indirect branch), so it
    • zonks the type it points to T{tc-tycon} Int -> Int, yielding T{knot-tied-tc} Int -> Int
    • and updates alpha to point to this zonked type.

The second step is a "small optimisation": there's no point in re-doing the work of zonking the type inside the Indirect if we encounter the variable a second time.

  • But alas, when we encounter alpha for a second time, we end up looking at T{knot-tied-tc} and fall into a black hole. The whole point of zonkTcTypeToType is that it produces a type full of knot-tied tycons, and you must not look at the result.

To put it another way zonkTcTypeToType . zonkTcTypeToType is not the same as zonkTcTypeToType. (If zonkTcTypeToType had different argumennt and result types, this issue would have been a type error; but the optimisation in zonkTyVarOcc would also become type-incorrect.)

Now I see the problem, I'm astonished that it has not bitten us before. It shows up in #15552 in a more complicated way than the one I describe here, involving unification inside kinds.

What to do?

I think the Right Thing is probably to follow the thought experiment of distinguishing Type from TcType. So then, instead of the current:

data MetaDetails
  = Flexi
  | Indirect TcType

we'd have to say

data MetaDetails
  = Flexi
  | IndirectTc TcType -- There may still be unification variables in here
  | Indirect   Type   -- No unification variables in here

This would mean that some 2-way branches become 3-way branches, so there might be a perf impact; I have no idea if it would be measurable.

Interestingly, zonkTcTypeToType could stop altogether (hooray, efficient) when it finds Indirect, whereas zonkTcType can't (sigh), because it can't tell if an IndirectTc is from "this" zonk or some earlier one. The only way I can see to solve that would be to count unifications, and record the current unification-count in the IndirectTc, thus IndirectTc UnifCount TcType. That would of course carry its own costs.

Any views? I'm going to wait a few days before doing anything drastic here.

Last edited 15 months ago by simonpj (previous) (diff)

comment:4 Changed 15 months ago by simonpj

In unravelling #15552 I also realised that

  • Note [Type checking recursive type and class declarations] in TcTyClsDecls uses the global type envt during zonking to hold the knot-tied TyCons
  • But the ZonkEnv used in TcHsSyn plays a very, very similar role
    data ZonkEnv
      = ZonkEnv
          UnboundTyVarZonker
          (TyCoVarEnv TyVar)
          (IdEnv      Var)         -- What variables are in scope
            -- Maps an Id or EvVar to its zonked version; both have the same Name
            -- Note that all evidence (coercion variables as well as dictionaries)
            --      are kept in the ZonkEnv
            -- Only *type* abstraction is done by side effect
            -- Is only consulted lazily; hence knot-tying
    

Moreover, as you'll see in TcHsSyn.zonkRecMonoBinds, the ZonkEnv is used in a knot-tied way, to get sharing of all the Ids.

My thought: we should use the same mechanism for both. The most straightforward thing is to add a NameEnv TyCon to ZonkEnv for those knot-tied TyCons. Then, in TcTyClDecls insetad of

  ; tcExtendRecEnv (zipRecTyClss tc_tycons rec_tyclss) $
    ...mapM (tcTyClDecl roles) tyclds...

we'd create a ZonkEnv, and pass it into tcTyClDecl. A little bit more plumbing, but more honest and certainly more uniform.

PS: it must be possible to get rid of that UnboundTyVarZonker field too.

comment:5 Changed 15 months ago by Simon Peyton Jones <simonpj@…>

In 184a569c/ghc:

Clean up TcHsSyn.zonkEnv

Triggered by Trac #15552, I'd been looking at ZonkEnv in TcHsSyn.

This patch does some minor refactoring

* Make ZonkEnv into a record with named fields, and use them.
  (I'm planning to add a new field, for TyCons, so this prepares
  the way.)

* Replace UnboundTyVarZonker (a higer order function) with the
  simpler and more self-descriptive ZonkFlexi data type, below.
 It's just much more perspicuous and direct, and (I suspect)
 a tiny bit faster too -- no unknown function calls.

data ZonkFlexi   -- See Note [Un-unified unification variables]
  = DefaultFlexi    -- Default unbound unificaiton variables to Any
  | SkolemiseFlexi  -- Skolemise unbound unification variables
                    -- See Note [Zonking the LHS of a RULE]
  | RuntimeUnkFlexi -- Used in the GHCi debugger

There was one knock-on effect in the GHCi debugger -- the
RuntimeUnkFlexi case.  Somehow previously, these RuntimeUnk
variables were sometimes getting SystemNames (and hence
printed as 'a0', 'a1', etc) and sometimes not (and hence
printed as 'a', 'b' etc).  I'm not sure precisely why, but
the new behaviour seems more uniform, so I just accepted the
(small) renaming wibbles in some ghci.debugger tests.

I had a quick look at perf: any changes are tiny.

comment:6 Changed 15 months ago by goldfire

Patch looks fine.

As for the larger plan: I like all of it, including separating TcType from Type. Could we also remove TcTyVar from the Var type? Then we could statically guarantee that no TcTyVars are in Core.

comment:7 Changed 15 months ago by simonpj

As for the larger plan: I like all of it

What is the "all of it" that you like, specifically? There are, I think, two pieces:

  1. Eliminate the bug. How? Current brand leader: add a third contructor to MetaDetails (comment:3). Do we have any other alternatives on the table?
  1. Clean up knot tying by using ZonkEnv (comment:4). This is pure refactoring, and hence not urgent, but it smells right to me.

comment:8 Changed 15 months ago by simonpj

Another idea for (1): just eliminate the "optimisation" in TcHsType.zonkTyVarOcc. Types generally have no sharing, so we may not be gaining much by increasing sharing her.

NB: in TcMType.zonkTcTyVar we could apply this optimisation; for some reason we don't even try to do that too.

Another idea: maintain (statefully) a map from (meta) TyVar to TyVar.

comment:9 Changed 15 months ago by goldfire

(written concurrently with commen:8)

After some discussion, Simon and I agreed that (1) from comment:7 would nab this bug. But many other questions/observations came up:

  1. This bug is caused by an optimization. What if we don't do the optimization? How much is performance affected? We hypothesize: not much. This is because while the optimization increases sharing in both time and space, this sharing is soon lost (in space, at least) in further passes.
  1. Interestingly, the other zonker (zonkTcType and friends in !TcMType) does not do this optimization. It could, and it wouldn't be plagued by this bug, as TyCons aren't zonked there. So we've done the optimization in precisely the places we shouldn't.
  1. The optimization doesn't quite go far enough. Consider alpha := beta -> beta and beta := Maybe (Int, Bool). Zonking alpha replaces the contents of the cell with Maybe (Int, Bool) -> Maybe (Int, Bool) instead of beta -> beta. But the next time we zonk alpha, we'll still walk over the large type Maybe (Int, Bool) -> Maybe (Int, Bool).

Simon and I puzzled on (C) for quite some time. We came up with a few approaches to implementing a better way to avoid redundant zonking. The key observation is that once we zonk alpha (and update its contents according to the current optimization), we don't have to do this again in the same zonk.

  1. We can track epoch numbers in the TcM monad (in a new mutable cell). The epoch would increase at every unification. Every Indirect node would store the epoch number of the type stored in the node -- that is, the type is fully zonked with respect to the stored epoch number. When zonking, if we encounter an Indirect whose epoch number matches the current epoch number, we know that the type is already zonked, and we can avoid traversing it.
  1. The idea in (a) doesn't apply only to filled-in metavariables, but to all types. The type-checker occasionally zonks types. However, if a type has already been zonked and there have been no unifications, then zonking it again is a waste of time. If we store an epoch number with every type, then we can check this against the global epoch number and skip some zonks.
  1. The idea in (b) is a bit heavy, though, requiring alternating proper Type nodes with epoch numbers in every type. Instead, we could just do this in TcTyVars, where we store the epoch number of their kind.
  1. An alternative to epoch numbers is to have each individual zonk track which variables' contents are already zonked. This could be done by adding an IORef TyVarEnv to the local environment to the zonk (replacing the () environment of a zonkTcType or adding to the ZonkEnv of a zonkTcTypeToType). Every time we zonk a variable, add the variable to the env't, mapping it to its fully-zonked contents (or, in the case of a TyVar, a version of the TyVar with a zonked kind).

With any of these ideas, it's not obvious that the work will be worth it, as it's hard to know how much redundant zonking we're doing.

comment:10 Changed 15 months ago by Simon Peyton Jones <simonpj@…>

In 565ef4c/ghc:

Remove knot-tying bug in TcHsSyn.zonkTyVarOcc

There was a subtle knot-tying bug in TcHsSyn.zonkTyVarOcc, revealed
in Trac #15552.

I fixed it by

* Eliminating the short-circuiting optimisation in zonkTyVarOcc,
  instead adding a finite map to get sharing of zonked unification
  variables.

  See Note [Sharing when zonking to Type] in TcHsSyn

* On the way I /added/ the short-circuiting optimisation to
  TcMType.zonkTcTyVar, which has no such problem.  This turned
  out (based on non-systematic measurements) to be a modest win.

  See Note [Sharing in zonking] in TcMType

On the way I renamed some of the functions in TcHsSyn:

* Ones ending in "X" (like zonkTcTypeToTypeX) take a ZonkEnv

* Ones that do not end in "x" (like zonkTcTypeToType), don't.
  Instead they whiz up an empty ZonkEnv.

comment:11 Changed 15 months ago by simonpj

Status: newmerge

OK I think I'm done with this. Perf is fine; and the bug is fixed. Lots of Notes to explain.

It fixes an outright bug, so merge if poss.

comment:12 Changed 14 months ago by RyanGlScott

Milestone: 8.6.18.6.2

Moving to the 8.6.2 milestone, since these tickets were all recently marked as merge.

comment:13 Changed 13 months ago by bgamari

Milestone: 8.6.28.6.1

This didn't end up happening for 8.6.1 due to its size. I suspect this won't change in 8.6.2.

Note: See TracTickets for help on using tickets.