#12549: Panic on ":t datatypeName" ---------------------------------+-------------------------------------- Reporter: johnleo | Owner: johnleo Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: Operating System: MacOS X | Architecture: x86_64 (amd64) Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | ---------------------------------+-------------------------------------- Comment (by johnleo): Note that this bug was "fixed" in https://git.haskell.org/ghc.git/commitdiff/f4a14d6c535bdf52b19f441fe185ea13d... (see https://ghc.haskell.org/trac/ghc/ticket/12785) by replacing `substTy` with `substTyUnchecked` in `new_meta_tv_x` (TcMType.hs). See below. Here is my understanding of the problem. The panic happens for example for this call: {{{ :set -XPolyKinds class C a where f :: a b c :type f }}} Unique names have been simplified for readability. The original type (all skolem variables) is the following: {{{ ∀ {kf} {kh} (a9 ∷ kf → kh → ★). C kf kh a9 ⇒ ∀ (ba ∷ kf) (cb ∷ kh). a9 ba cb }}} The outer call to deeply instantiate substitutes `kf -> kj, kh -> kk, a9 -> al` where the new variables are all tau. Theta becomes `C kj kk al` and we call `deeplyinstantiate` now on `∀ (ba ∷ kj) (cb ∷ kk). al ba cb` where it attempts to substitute `ba -> bp, cb -> cq` Substitutions are created by `newMetaTyVars` which is defined as follows. {{{ newMetaTyVars = mapAccumLM newMetaTyVarX emptyTCvSubst -- emptyTCvSubst has an empty in-scope set, but that's fine here -- Since the tyvars are freshly made, they cannot possibly be -- captured by any existing for-alls. }}} Note the comment: `kj` and `kk` are free variables in the range of the upcoming substitutions but are not part of the in-scope set. They were however "freshly made" in the outer call. Now `newMetaTyVarX` calls `new_meta_tv_x` which includes this line (before SPJ's change): {{{ kind = substTy subst (tyVarKind tv) }}} Note that `subst` at this point contains the substitutions made prior to the current one, and so is originally empty. So `substTy` succeeds on `ba -> bp` (with kind `kj`), and `bp` and `kj` are added to the in-scope set. However on the second attempt `cb -> cq` (with kind `kk`), since `subst` is now non-empty, `substTy` calls `checkValidSubst` with arguments `subst` and `[kk]`. `checkValidSubst` does two checks, the second of which (`tysColsFVsInScope`) fails. This checks that `kk` is in the in-scope set which consists of `{kj, bp}`, and thus the panic. Although I understand the problem, I don't know the best way to fix it. Certainly retaining `kk` and the others in the in-scope set for the recursive call to `deeplyInstantiate` would be sufficient, but I'm not sure why it's necessary. No real substitution is being done for `kk` at this point, so it is not clear why we need to check the substitution invariant. And even if there was a substitution since the variables are fresh there should no risk of capture during alpha-renaming. While I was investigating this, SPJ made the change mentioned at the top of this note, which is: {{{ kind = substTyUnchecked subst (tyVarKind tv) -- Unchecked because we call newMetaTyVarX from -- tcInstBinderX, which is called from tc_infer_args -- which does not yet take enough trouble to ensure -- the in-scope set is right; e.g. Trac #12785 trips -- if we use substTy here }}} This indicates that there is a more wide-spread problem, so I don't want to make any changes that would break something else. I'm happy to investigate fixing the larger problem, however. In any case I'd appreciate some guidance at this point. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12549#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler