Kind inference crash
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
andD
are mutually recursive -
ka
andkb
get bound to unification variables, and then get unified in the kind-inference phase - As a result the utterly-final class for
C
andD
end up with the sameTyVar
forka
/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.