blob: 72c208d77d90966790070db2d3e43b76e2985924 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
|
{-# LANGUAGE Haskell2010 #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
-- The code from the ticket lacked these extensions,
-- but crashed the compiler with "GHC internal error"
-- It doesn't crash now; and in this test case I've added
-- the extensions, which makes it compile cleanly
{-# LANGUAGE FlexibleContexts, FlexibleInstances, UndecidableInstances, FunctionalDependencies #-}
module T12055 where
import Data.Kind (Constraint, Type)
import Data.Type.Equality (type (~), 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)
|
