Skip to content

Ghc panic: Kind application error in type SelfDom IO (DefaultCat *)

I have not trimmed this down, but enabling StandaloneKindSignatures and adding a kind signature to SelfDom results in a panic:

type SelfDom :: (i -> j) -> Cat i -> Cat i
type family SelfDom (f :: i -> j) (k :: Cat i) :: Cat i where
  SelfDom p p = Op p
  SelfDom f p = p
$ ghci -ignore-dot-ghci hs/3461.hs
GHCi, version 8.10.0.20191123: https://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Data.Category.Functor ( hs/3461.hs, interpreted )
ghc: panic! (the 'impossible' happened)
  (GHC version 8.10.0.20191123:
	Core Lint error
  <no location info>: warning:
      Kind application error in type ‘SelfDom IO (DefaultCat *)’
        Function kind = forall i j. (i -> j) -> Cat i -> Cat i
        Arg kinds = [(*, *), (j_a1ee, *), (IO, * -> *),
                     (DefaultCat *, Cat *)]
      Fun: * -> j_a1ee
           (IO, * -> *)
      In the type ‘SelfDom IO (DefaultCat *)’
      Substitution: [TCvSubst
                       In scope: InScope {j_a1ee}
                       Type env: []
                       Co env: []]
  Dom
  [TCvSubst
     In scope: InScope {j_a1ee}
     Type env: [a19f :-> j_a1ee]
     Co env: []]
  [j_a1ee]
  []
  [j_a1ee, *, IO]
  SelfDom IO (DefaultCat *)
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:1179:37 in ghc:Outputable
        pprPanic, called at compiler/typecheck/FamInst.hs:184:31 in ghc:FamInst

Please report this as a GHC bug:  https://www.haskell.org/ghc/reportabug

>

I apologize for the length of the code:

{-# Options_GHC -dcore-lint #-}
{-# Language StandaloneKindSignatures #-}
{-# Language MultiParamTypeClasses #-}
{-# Language FlexibleInstances #-}
{-# Language FlexibleContexts #-}
{-# Language FunctionalDependencies #-}
{-# Language UndecidableInstances #-}
{-# Language UndecidableSuperClasses #-}
{-# Language RankNTypes #-}
{-# Language KindSignatures #-}
{-# Language PolyKinds #-}
{-# Language DataKinds #-}
{-# Language TypeOperators #-}
{-# Language TypeFamilies #-}
{-# Language GADTs #-}
{-# Language ScopedTypeVariables #-}
{-# Language DefaultSignatures #-}
{-# Language ImportQualifiedPost #-}
{-# Language TypeFamilyDependencies #-}
{-# Language StandaloneDeriving #-}
{-# Language DerivingStrategies #-}
{-# Language GeneralizedNewtypeDeriving #-}
{-# Language DerivingVia #-}
{-# Language BlockArguments #-}
{-# Language RoleAnnotations #-}
module Data.Category.Functor
  ( Functor(..)
  , ob
  , FunctorOf
  , contramap
  , SelfDom
  , DefaultCat
  , type (~>)
  , Nat(..)
  , Hom(..)
  ) where

import Data.Constraint
import GHC.Types hiding (Nat)
import Prelude hiding (Functor(..),map,id,(.))
import Prelude qualified
import Control.Category qualified as Control

class Trivial (k :: i -> i -> Type) (a :: i)
instance Trivial k a

type Cat i = i -> i -> Type

class 
  ( Op (Op k) ~ k
  , Ob (Op k) ~ Ob k
  , Category (Op k)
  ) => Category (k :: Cat i) where
  type Ob k :: i -> Constraint
  type Ob k = Trivial k

  type Op k :: i -> i -> Type
  type Op k = Y k

  id :: Ob k a => k a a
  default id :: (Control.Category k, Ob k ~ Trivial k, Ob k a) => k a a
  id = Control.id

  (.) :: k b c -> k a b -> k a c
  default (.) :: (Control.Category k, Ob k ~ Trivial k, Ob k a) => k b c -> k a b -> k a c
  (.) = (Control..)

  src :: k a b -> Dict (Ob k a)
  default src :: (Ob k ~ Trivial k) => k a b -> Dict (Ob k a)
  src _ = Dict

  tgt :: k a b -> Dict (Ob k b)
  default tgt :: (Ob k ~ Trivial k) => k a b -> Dict (Ob k b)
  tgt _ = Dict

  op :: k a b -> Op k b a
  default op :: (Op k ~ Y k) => k a b -> Op k b a
  op = Y

  unop :: Op k b a -> k a b
  default unop :: (Op k ~ Y k) => Op k b a -> k a b
  unop (Y f) = f

newtype Y k a b = Y (k b a)

instance (Category k, Op k ~ Y k) => Category (Y k) where
  type Op (Y k) = k
  type Ob (Y k) = Ob k
  id = Y id
  Y f . Y g = Y (g . f)
  src (Y f) = tgt f
  tgt (Y f) = src f
  op (Y f) = f
  unop = Y

instance Category (:-)

instance Category (->)

type SelfDom :: (i -> j) -> Cat i -> Cat i
type family SelfDom (f :: i -> j) (k :: Cat i) :: Cat i where
  SelfDom p p = Op p
  SelfDom f p = p

type family DefaultCat (i :: Type) = (res :: Cat i) | res -> i
type instance DefaultCat Type = (->)
type instance DefaultCat Constraint = (:-)
type instance DefaultCat (i -> j) = Nat (DefaultCat i) (DefaultCat j)

class
  ( Category (Dom f)
  , Category (Cod f)
  ) => Functor (f :: i -> j) where

  type Dom f :: Cat i
  type Dom (f :: i -> j) = SelfDom f (DefaultCat i)

  type Cod f :: Cat j
  type Cod (f :: i -> j) = DefaultCat j

  map :: Dom f a b -> Cod f (f a) (f b)
  default map :: (f ~~ g, Prelude.Functor g, Dom f ~~ (->), Cod f ~~ (->)) => Dom f a b -> Cod f (f a) (f b)
  map = Prelude.fmap

ob :: forall f a. Functor f => Ob (Dom f) a :- Ob (Cod f) (f a)
ob = Sub $ case src (map id :: Cod f (f a) (f a)) of Dict -> Dict

contramap :: Functor f => Op (Dom f) b a -> Cod f (f a) (f b)
contramap = map . unop

class    (Functor f, Dom f ~ p, Cod f ~ q) => FunctorOf p q f | f -> p q
instance (Functor f, Dom f ~ p, Cod f ~ q) => FunctorOf p q f

type (f :: i -> j) ~> (g :: i -> j) = Nat (DefaultCat i) (DefaultCat j)

data Nat (p :: Cat i) (q :: Cat j) (f :: i -> j) (g :: i -> j)
  = (FunctorOf p q f, FunctorOf p q g) => Nat { runNat :: forall a. Ob p a => q (f a) (g a) }

instance (Category p, Category q) => Category (Nat p q) where
  type Ob (Nat p q) = FunctorOf p q
  id = Nat id1 where
    id1 :: forall f x. (FunctorOf p q f, Ob p x) => q (f x) (f x)
    id1 = id \\ (ob :: Ob p x :- Ob q (f x))
  Nat f . Nat g = Nat (f . g)
  src Nat{} = Dict
  tgt Nat{} = Dict

instance (Category p, Category q) => Functor (Nat p q) where
  type Dom (Nat p q) = Y (Nat p q)
  type Cod (Nat p q) = Nat (Nat p q) (->)
  map (Y f) = Nat (. f)

instance (Category p, Category q) => Functor (Nat p q f) where
  type Dom (Nat p q f) = Nat p q
  type Cod (Nat p q f) = (->)
  map = (.)


newtype Hom (k :: Cat i) (a :: i) (b :: i) = Hom { runHom :: k a b }
type role Hom representational nominal nominal

-- deriving instance Category k => Category (Hom k)
{-
instance Category k => Category (Hom k) where
  type Ob (Hom k) = Ob k
  type Op (Hom k) = Hom (Op k)
  id = Hom id
  Hom f . Hom g = Hom (f . g)
  src (Hom f) = src f
  tgt (Hom f) = tgt f
  op (Hom f) = Hom (op f)
  unop (Hom f) = Hom (unop f)
-}



instance Category k => Functor (Hom k e :: i -> Type) where
  type Dom (Hom k e) = k
  type Cod (Hom k e) = (->)
  map f (Hom g) = Hom (f . g)

instance Category k => Functor (Hom k :: i -> i -> Type) where
  type Dom (Hom k) = Op k
  type Cod (Hom k) = Nat k (->)
  map f = Nat \(Hom g) -> Hom (g . unop f)


instance Functor ((->) e)

-- deriving via (Hom (->)) instance Functor (->)
instance Functor (->) where map f = Nat (. unop f)

instance (Category p, Op p ~ Y p) => Functor (Y p a) where
  type Dom (Y p a) = Y p
  type Cod (Y p a) = (->)
  map = (.)

instance (Category p, Op p ~ Y p) => Functor (Y p) where
  type Dom (Y p) = p
  type Cod (Y p) = Nat (Y p) (->)
  map f = Nat (. Y f)

instance Functor Dict where
  map p Dict = case p of
    Sub q -> q

instance Functor ((:-) e) where
  map = (.)

instance Functor (:-) where
  map (Y f) = Nat (. f)

instance Functor ((,) e)
instance Functor (Either e)
instance Functor []
instance Functor Prelude.Maybe
instance Functor IO
instance Functor (,) where
  map f = Nat \(a,b) -> (f a, b)

instance Functor Either where
  map f0 = Nat (go f0) where
    go :: (a -> b) -> Either a c -> Either b c
    go f (Left a)  = Left (f a)
    go _ (Right b) = Right b
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information