Skip to content

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

Edited by Simon Peyton Jones
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information