Вложенное программирование на уровне уровня

Question

Я пытаюсь использовать DataKinds для программирования на уровне уровня, но я сталкиваюсь с трудностями, когда у меня есть одна из этих структур, вложенных в другую.

{-# 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

Или вы могли бы написать свой ClassLower экземпляр, как это, используя поиск по шаблону (а не переменной типа), чтобы различать случаи GADT:

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

Answer 2

Проблема здесь немного тонкая. Причина, по которой можно ожидать, что GHC согласится с этим, заключается в том, что у вас есть экземпляры для всех возможных Lower a, поскольку вы предоставляете только способы сделать Lower D и Lower E. Тем не менее, можно было бы построить патологический определение для 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 действительно не может быть уверен, что ClassLower (Lower a) ограничение (необходимо из-за использования somefunc2) будет удовлетворено. Для этого ему нужно будет выполнить небольшую работу по проверке конструкторов GADT и убедиться, что все возможные случаи охватываются каким-то экземпляром.

В этом случае вы можете решить вашу проблему, добавив ограничение ClassLower (Lower a) к конструктору GADT (разрешение FlexibleContexts).

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