從ADT中恢復GADT時出現的類型問題

Question

我想將我輸入的GADT（GExpr）放入哈希映射中，因此我首先將其轉換爲相應的單形ADT（Expr）。當我從hashmap中查找時，我很難將單形ADT轉換回GADT。

以下是簡化版本。基本上有兩個功能，「昏暗」和「gexprOfExpr」，我只能讓他們中的一個立即工作。我試圖做什麼不可能？

{-# OPTIONS_GHC -Wall #-} 
{-# Language GADTs #-} 

type ListDim = [Int] 

data DIM0 = DIM0 
data DIM1 = DIM1 

class Shape sh where 
    shapeOfList :: ListDim -> sh 

instance Shape DIM0 where 
    shapeOfList _ = DIM0 
instance Shape DIM1 where 
    shapeOfList _ = DIM1 

data Expr = EConst ListDim Double 
      | ESum ListDim Int 

data GExpr sh where 
    GRef :: sh -> Int -> GExpr sh 
    GConst :: sh -> Double -> GExpr sh 
    GSum :: GExpr DIM1 -> GExpr DIM0 -- GADT, this works for "dim" 
-- GSum :: GExpr DIM1 -> GExpr sh -- phantom type, this works for "gexprOfExpr" 

dim :: GExpr sh -> sh 
dim (GRef sh _) = sh 
dim (GConst sh _) = sh 
dim (GSum _) = DIM0 

gexprOfExpr :: Shape sh => Expr -> GExpr sh 
gexprOfExpr (EConst lsh x) = GConst (shapeOfList lsh) x 
gexprOfExpr (ESum lsh k) = GSum $ GRef (shapeOfList lsh) k 

注：我知道我正在嘗試恢復的類型。如果它將幫助，這將是罰款：

從#haskell

gexprOfExpr :: Shape sh => sh -> Expr -> GExpr sh 

Answer 1

Saizan給了我一個提示，直接給出答案。這裏的工作版本：

{-# OPTIONS_GHC -Wall #-} 
{-# Language GADTs #-} 

import Data.Maybe 

type ListDim = [Int] 

data DIM0 = DIM0 
data DIM1 = DIM1 

class Shape sh where 
    shapeOfList :: ListDim -> sh 
    maybeGExprOfExpr :: Expr -> Maybe (GExpr sh) 
    maybeGExprOfExpr _ = Nothing 

instance Shape DIM0 where 
    shapeOfList _ = DIM0 
    maybeGExprOfExpr (ESum lsh k) = Just $ GSum $ GRef (shapeOfList lsh) k 
    maybeGExprOfExpr _ = Nothing 

instance Shape DIM1 where 
    shapeOfList _ = DIM1 


data Expr = EConst ListDim Double 
      | ESum ListDim Int 

data GExpr sh where 
    GRef :: sh -> Int -> GExpr sh 
    GConst :: sh -> Double -> GExpr sh 
    GSum :: GExpr DIM1 -> GExpr DIM0 

dim :: GExpr sh -> sh 
dim (GRef sh _) = sh 
dim (GConst sh _) = sh 
dim (GSum _) = DIM0 

gexprOfExpr :: Shape sh => Expr -> GExpr sh 
gexprOfExpr (EConst lsh x) = GConst (shapeOfList lsh) x 
gexprOfExpr e@(ESum _ _) = fromJust $ maybeGExprOfExpr e