Typechecker panic instead of proper error
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)’