[GHC] #12549: Panic on ":t datatypeName"

[GHC]

#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/f4a14d6c535bdf52b19f441fe185ea13d62fdc24
 (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