
#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