Skip to content

Type checker crash

This program

{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}

module Main where
import Data.Kind (Constraint, Type)

data family Pi t :: Type

type FunctionSymbol :: Type -> Type
type FunctionSymbol t = Type

type IsSum :: forall s. FunctionSymbol s -> Constraint
class IsSum (sumf :: FunctionSymbol t) where
    sumConNames :: Pi t

crashes GHC like this:

generic-bug.hs:15:23: error: []8;;https://errors.haskell.org/messages/GHC-76329\GHC-76329]8;;\]
    • GHC internal error: ‘t’ is not in scope during type checking, but it passed the renamer
      tcl_env of environment: [ahc :-> Type variable ‘sumf’ = sumf :: FunctionSymbol
                                                                        s,
                               awz :-> Type variable ‘s’ = s :: *,
                               rh7 :-> ATcTyCon IsSum :: forall s. FunctionSymbol s -> Constraint]
    • In the first argument of ‘Pi’, namely ‘t’
      In the type signature: sumConNames :: Pi t
      In the class declaration for ‘IsSum’
   |
15 |     sumConNames :: Pi t
   |                       ^

HEAD, 9.8, 9.6, all of them!

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