[GHC] #16342: Kind inference crash

[GHC]

#16342: Kind inference crash
-------------------------------------+-------------------------------------
        Reporter:  simonpj           |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.6.3
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Description changed by simonpj:

Old description:

> 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.

New description:

 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 outright, 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#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler