[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):

 Thank you, that is indeed very helpful.  I agree that comment in
 `newMetaTyVars` is very likely
 incorrect and the source of bugs.  However I believe the panic that occurs
 in this case is
 actually a different problem.  First note that the actual substitutions of
 the kinds that results
 in `∀ (ba ∷ kj) (cb ∷ kk). al ba cb` happens earlier, on the line
 {{{
 ; (wrap2, rho2) <- deeplyInstantiate orig (substTyUnchecked subst rho)
 }}}
 of `deeplyInstantiate`.  Note that the substitution was already unchecked
 there, likely due to
 the problem you mention (as well as perhaps other problems).  The panic in
 the line
 {{{
 kind   = substTy subst (tyVarKind tv)
 }}}
 that happens later seems unrelated to the substitution invariant.  At this
 point the kinds
 have already been substituted, so it is trying to do the substitution `kk
 -> kk`, which
 in fact satisfies the invariant.  The code line above is very suspicious
 to me--I'm not sure why
 any substitution for the kind is being attempted.  Why not just `kind =
 tyVarKind tv`?
 If all kinds must be specified before the types that use them (and I
 assume that is checked
 somewhere earlier) then the kind substitution must have already been
 happened.

 The problem seems to be that `subst` here is the substitution for the type
 variable, but
 we pass in the kind variable as the second argument to `substTy` which
 confuses
 `checkValidSubst`.  This can be seen from the values printed out by the
 assert (here with
 the full names).
 {{{
   in_scope InScope {k_a12j b_a12p}
   tenv [a11a :-> b_a12p[tau:2]]
   cenv []
   tys [k_a12k[tau:2]]
   cos []
   needInScope [a12k :-> k_a12k[tau:2]]
 }}}
 The substitution being attempted is `kk -> kk` but `tenv` contains the `ba
 -> bp` substitution.
 So in the lines
 {{{
   needInScope = (tyCoVarsOfTypes tys `unionVarSet` tyCoVarsOfCos cos)
                   `delListFromUFM_Directly` substDomain
 }}}
 of `checkValidSubst` the `substDomain` (of `tenv`) is getting removed from
 `needInScope` but it is the
 wrong domain--it should be `kk`, not `ba`.

 Anyway it seems there seem to be a lot of problems with this code, and
 it's certainly worth
 going through and cleaning up, but again I'd appreciate some perspective
 to make sure I'm
 not breaking more than I fix.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12549#comment:18>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler