GHC：ファントム型のパラメータを推測できない

Question

可変長のタプルの型を作成しようとしています。基本的には、Either a (Either (a,b) (Either (a,b,c) ...))とEither (Either (Either ... (x,y,z)) (y,z)) zというよりきれいなバージョンです。

{-# LANGUAGE TypeOperators, TypeFamilies, MultiParamTypeClasses, FlexibleInstances #-} 
module Temp where 

-- type level addition 
data Unit 
data Succ n 

class Summable n m where 
    type Sum n m :: * 

instance Summable Unit m where 
    type Sum Unit m = Succ m 

instance Summable n m => Summable (Succ n) m where 
    type Sum (Succ n) m = Succ (Sum n m) 

-- variable length tuple, left-to-right 
data a :+ b = a :+ Maybe b 
infixr 5 :+ 

class Prependable t r s where 
    type Prepend t r s :: * 
    prepend :: r -> Maybe s -> Prepend t r s 

instance Prependable Unit x y where 
    type Prepend Unit x y = x :+ y 
    prepend = (:+) 

instance Prependable n x y => Prependable (Succ n) (w :+ x) y where 
    type Prepend (Succ n) (w :+ x) y = w :+ Prepend n x y 
    prepend (w :+ Nothing) _ = w :+ Nothing 
    prepend (w :+ Just x) y = w :+ Just (prepend x y) 

-- variable length tuple, right-to-left 
data a :- b = Maybe a :- b 
infixl 5 :- 

class Appendable t r s where 
    type Append t r s :: * 
    append :: Maybe r -> s -> Append t r s 

instance Appendable Unit x y where 
    type Append Unit x y = x :- y 
    append = (:-) 

instance Appendable n x y => Appendable (Succ n) x (y :- z) where 
    type Append (Succ n) x (y :- z) = Append n x y :- z 
    append _ (Nothing :- z) = Nothing :- z 
    append x (Just y :- z) = Just (append x y) :- z 

しかし、コンパイラは、再帰的な例でprependまたはappendのファントム型パラメータを推測することができないようだ：

Temp.hs:32:40: 
    Could not deduce (Prepend t1 x y ~ Prepend n x y) 
    from the context (Prependable n x y) 
     bound by the instance declaration at Temp.hs:29:10-61 
    NB: `Prepend' is a type function, and may not be injective 
    In the return type of a call of `prepend' 
    In the first argument of `Just', namely `(prepend x y)' 
    In the second argument of `(:+)', namely `Just (prepend x y)' 

Temp.hs:49:34: 
    Could not deduce (Append t0 x y ~ Append n x y) 
    from the context (Appendable n x y) 
     bound by the instance declaration at Temp.hs:46:10-59 
    NB: `Append' is a type function, and may not be injective 
    In the return type of a call of `append' 
    In the first argument of `Just', namely `(append x y)' 
    In the first argument of `(:-)', namely `Just (append x y)' 

は、私は、コンパイラは、この推論を作るのを助けるために何かできることはありますか？

Answer 1

ここでエラーメッセージの重要な部分がある：

NB: `Prepend' is a type function, and may not be injective 

これは何を意味するのでしょうか？複数のinstance Prependableがあり、type Prepend ... = aとなる可能性があるので、Prependをaと推測すると、そのインスタンスが必ずしも属しているとは限りません。

あなたは（あなたが全射ですがは単射であるかもしれないし、代わりに全単射あるタイプの「関係」、とのタイプの機能に対処していないという利点があるdata types in type familiesを、使用してので、すべてをこの問題を解決することができますPrependタイプは1つのタイプファミリーにのみ属し、すべてのタイプファミリーには別のPrependタイプがあります）。

（あなたは私のタイプの家族内のデータ型を持つソリューションを表示したい場合は、コメントを残し！基本的には、だけではなく、type Prependのdata Prependを使用）

Answer 2

私が思いついた解決策は、仮引数を追加しましたファントムパラメータにprependとappendを結びつけるために：

-- as above, except... 

unsucc :: Succ n -> n 
unsucc _ = undefined 

class Prependable t r s where 
    type Prepend t r s :: * 
    prepend :: t -> r -> Maybe s -> Prepend t r s 

instance Prependable Unit x y where 
    type Prepend Unit x y = x :+ y 
    prepend _ = (:+) 

instance Prependable n x y => Prependable (Succ n) (w :+ x) y where 
    type Prepend (Succ n) (w :+ x) y = w :+ Prepend n x y 
    prepend _ (w :+ Nothing) _ = w :+ Nothing 
    prepend t (w :+ Just x) y = w :+ Just (prepend (unsucc t) x y) 

class Appendable t r s where 
    type Append t r s :: * 
    append :: t -> Maybe r -> s -> Append t r s 

instance Appendable Unit x y where 
    type Append Unit x y = x :- y 
    append _ = (:-) 

instance Appendable n x y => Appendable (Succ n) x (y :- z) where 
    type Append (Succ n) x (y :- z) = Append n x y :- z 
    append _ _ (Nothing :- z) = Nothing :- z 
    append t x (Just y :- z) = Just (append (unsucc t) x y) :- z