[GHC] #16342: Kind inference crash

20 Feb 2019

      #16342: Kind inference crash
-------------------------------------+-------------------------------------
           Reporter:  simonpj        |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.6.3
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Here's a gnarly test case
 {{{
 {-# LANGUAGE MultiParamTypeClasses, TypeInType, ConstrainedClassMethods,
 ScopedTypeVariables #-}

 module Foo where

 import Data.Proxy

 class C (a::ka) x where
   cop :: D a x => x -> Proxy a -> Proxy a
   cop _ x = x :: Proxy (a::ka)

 class D (b::kb) y where
   dop :: C b y => y -> Proxy b -> Proxy b
   dop _ x = x :: Proxy (b::kb)
 }}}
 This crashes every recent GHC with
 {{{
     • GHC internal error: ‘kb’ is not in scope during type checking, but
 it passed the renamer
       tcl_env of environment: [avu :-> Type variable ‘b’ = b :: ka,
                                avv :-> Type variable ‘y’ = y :: *,
                                avw :-> Identifier[x::Proxy b,
 NotLetBound],
                                avx :-> Type variable ‘ka’ = ka :: *]
     • In the kind ‘kb’
       In the first argument of ‘Proxy’, namely ‘(b :: kb)’
       In an expression type signature: Proxy (b :: kb)
    |
 13 |   dop _ x = x :: Proxy (b::kb)
    |                            ^^
 }}}
 Yikes.

 Reason:
 * `C` and `D` are mutually recursive
 * `ka` and `kb` get bound to unification variables, and then get unified
 in the kind-inference phase
 * As a result the utterly-final class for `C` and `D` end up with the same
 `TyVar` for `ka`/`kb`.
 * And then, for one of them, the tyvar is not in scope when (much, much
 later) we check the default declaration.

 Gah!  In `generaliseTcTyCon` I think we may need to do a reverse-map to
 ensure that each of the final `tyConTyVars` has the `Name` from this
 declaration, rather than accidentally getting a `Name` from another decl
 in the mutually recursive group.

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16342
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler