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