GitLab

Consider this modification of the testcase from #12021,

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeInType #-}

import GHC.Base ( Constraint, Type )
import GHC.Exts ( type (~~) )

type Cat k = k -> k -> Type

class Category (p :: Cat k) where
    type Ob p :: k -> Constraint

class (Category (Dom f), Category (Cod f)) => Functor (f :: j -> k) where
    type Dom f :: Cat j
    type Cod f :: Cat k
    functor :: forall a b.
               Iso Constraint (:-) (:-)
               (Ob (Dom f) a)     (Ob (Dom f) b)
               (Ob (Cod f) (f a)) (Ob (Cod f) (f b))

class (Functor f , Dom f ~ p, Cod f ~ q) =>
    Fun (p :: Cat j) (q :: Cat k) (f :: j -> k) | f -> p q
instance (Functor f , Dom f ~ p, Cod f ~ q) =>
    Fun (p :: Cat j) (q :: Cat k) (f :: j -> k)

data Nat (p :: Cat j) (q :: Cat k) (f :: j -> k) (g :: j -> k)

type Iso k (c :: Cat k) (d :: Cat k) s t a b =
    forall p. (Cod p ~~ Nat d (->)) => p a b -> p s t

data (p :: Constraint) :- (q :: Constraint)

With GHC 8.0.1 it fails with a compiler panic,

$ ghc Hi.hs -fprint-explicit-kinds
[1 of 1] Compiling Main             ( Hi.hs, Hi.o )

Hi.hs:21:1: error:
    • Non type-variable argument
        in the constraint: Category j (Dom k j f)
      (Use FlexibleContexts to permit this)
    • In the context: (Category j (Dom k j f), Category k (Cod k j f))
      While checking the super-classes of class ‘Functor’
      In the class declaration for ‘Functor’

Hi.hs:29:20: error:
    • GHC internal error: ‘Dom’ is not in scope during type checking, but it passed the renamer
      tcl_env of environment: [a2yi :-> Type variable ‘j’ = j,
                               a2yj :-> Type variable ‘p’ = p, a2yk :-> Type variable ‘k’ = k,
                               a2yl :-> Type variable ‘q’ = q, a2ym :-> Type variable ‘f’ = f,
                               r2xT :-> ATcTyCon Fun]
    • In the first argument of ‘~’, namely ‘Dom f’
      In the class declaration for ‘Fun’

If one adds the appropriate extensions (FunctionalDependencies, FlexibleInstances, and FlexibleContexts) GHC complains that the program fails to satisfy the coverage condition,

Hi.hs:31:10: error:
    • Illegal instance declaration for ‘Fun k j p q f’
        The coverage condition fails in class ‘Fun’
          for functional dependency: ‘f -> p q’
        Reason: lhs type ‘f’ does not determine rhs types ‘p’, ‘q’
        Un-determined variables: p, q
        Using UndecidableInstances might help
    • In the instance declaration for
        ‘Fun (p :: Cat j) (q :: Cat k) (f :: j -> k)’