时间戳

首页 > 解决方案 > 如何解决冲突的类型族实例声明

haskell - 如何解决冲突的类型族实例声明

问题描述

我正在尝试以 Edward Kmett 的Hask制作一种多态类别理论。在尝试翻译和现代化 Functor Composition 时，我遇到了 GHC 认为类型族实例重叠的问题。有没有办法解决以下问题？

{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Hask.Functor.Compose where

import qualified Prelude as Base
import Data.Kind (Type)

-- The Type of Categories
type Cat i = i -> i -> Type

-- Natural Transformations
data Nat (p :: Cat i) (q :: Cat j) (f :: i -> j) (g :: i -> j) :: Type where

-- Hail Satan
data family Any :: k

data COMPOSE = Compose
type Compose = (Any 'Compose :: Cat i -> Cat j -> Cat k -> (j -> k) -> (i -> j) -> (i -> k))

-- Simplified Functor
class Functor (f :: i -> j) where
  type Dom f :: Cat i

instance Functor (Compose p q r f g) where
  type Dom (Compose p q r f g) = p

instance Functor (Compose p q r f) where
  type Dom (Compose p q r f) = Nat p q

错误：

Preprocessing library for kpf-0.1.0..
Building library for kpf-0.1.0..
[6 of 6] Compiling Hask.Functor.Compose ( Hask/Functor/Compose.hs, dist/build/Hask/Functor/Compose.o )

Hask/Functor/Compose.hs:30:8: error:
    Conflicting family instance declarations:
      forall j1 i j2 (p :: Cat i) (q :: Cat j1) (r :: Cat j2) (f :: j1
                                                                -> j2) (g :: i -> j1).
        Dom (Compose p q r f g) = p
          -- Defined at Hask/Functor/Compose.hs:30:8
      forall j i k (p :: Cat i) (q :: Cat j) (r :: Cat k) (f :: j -> k).
        Dom (Compose p q r f) = Nat p q
          -- Defined at Hask/Functor/Compose.hs:33:8
   |
30 |   type Dom (Compose p q r f g) = p
   |        ^^^

完整的未简化代码可以在这里找到。

标签： haskelldependent-typecategory-theory

解决方案

推荐阅读