ネストされた型レベルプログラミング

Question

データ型を使用して型レベルプログラミングを行っていますが、これらの構造体を別の構造体に入れ子にしていると難しいです。

{-# LANGUAGE DataKinds, TypeFamilies, GADTs, MultiParamTypeClasses, FlexibleInstances #-} 

module Temp where 

data Prop1 = D | E 

data Lower :: Prop1 -> * where 
    SubThing1 :: Lower D 
    SubThing2 :: Lower E 

class ClassLower a where 
    somefunc2 :: a -> String 

instance ClassLower (Lower D) where 
    somefunc2 a = "string3" 

instance ClassLower (Lower E) where 
    somefunc2 a = "string4" 

data Prop2 = A | B | C 

data Upper :: Prop2 -> * where 
    Thing1 :: Upper A 
    Thing2 :: Upper B 
    Thing3 :: Lower a -> Upper C 

class ClassUpper a where 
    somefunc :: a -> String 

instance ClassUpper (Upper A) where 
    somefunc a = "string1" 

instance ClassUpper (Upper B) where 
    somefunc a = "string2" 

instance ClassUpper (Upper C) where 
    somefunc (Thing3 x) = somefunc2 x 

最後にClassUpperのインスタンスを追加すると、エラーが発生します。

Temp.hs:37:25: error: 
    • Could not deduce (ClassLower (Lower a)) 
     arising from a use of ‘somefunc2’ 
     from the context: 'C ~ 'C 
     bound by a pattern with constructor: 
        Thing3 :: forall (a :: Prop1). Lower a -> Upper 'C, 
       in an equation for ‘somefunc’ 
     at /Users/jdouglas/jeff/emulator/src/Temp.hs:37:13-20 
    • In the expression: somefunc2 x 
     In an equation for ‘somefunc’: somefunc (Thing3 x) = somefunc2 x 
     In the instance declaration for ‘ClassUpper (Upper 'C)’ 

私は解決策や回避策を'C ~ 'Cは平等を入力示しますが、私は根本的な問題が何であるかを理解していない、はるかに少ないことを理解しています。

私は理解していないことと、この問題に取り組む最も良い方法は何ですか？

Answer 1

それとも、GADTの例を区別するために（むしろ型変数より）パターンマッチングを使用して、このようなあなたのClassLowerインスタンスを書き出すことができます：

instance ClassLower (Lower a) where 
    somefunc2 SubThing1 = "string3" 
    somefunc2 SubThing2 = "string4" 

Answer 2

ここの問題は少し微妙です。 GHCがこれを受け入れると思われる理由は、Lower DとLower Eの方法しか提供していないので、すべての可能性のあるインスタンスがあることです。Lower aしかし、1はLower

よう

import GHC.Exts (Any) 

data Lower :: Prop1 -> * where 
    SubThing1 :: Lower D 
    SubThing2 :: Lower E 
    SubThing3 :: Lower Any 

のための病理学的な定義を構築することができポイントがないだけDとEは親切Prop1を持っているということです。 Anyのようなものだけではなく、次のコンストラクタさえ許されています（F Int :: Prop1もそうです）！

SubThing4 :: Lower (F Int) 

type family F x :: Prop1 where {} 

ので、要約では、根本的な問題は、GHCが本当に（原因somefunc2の使用に必要な）ClassLower (Lower a)制約を満たすことになるだろうされていることを確認することができないということです。これを行うには、GADTコンストラクタをチェックし、すべての可能性のあるケースがいくつかのインスタンスでカバーされていることを確認する作業が必要です。

この場合、ClassLower (Lower a)という制約をGADTコンストラクタ（FlexibleContextsを有効にする）に追加することで問題を解決できます。

data Upper :: Prop2 -> * where 
    Thing1 :: Upper A 
    Thing2 :: Upper B 
    Thing3 :: ClassLower (Lower a) => Lower a -> Upper C