Type when restoring GADT from ADT

Question

I want to put my typed GADT (GExpr) in a hash map, so first I convert it to the corresponding monomorphic ADT (Expr). When I look at the hash map, I am having problems converting monomorphic ADT back to GADT.

The following is a simplified version. Essentially, there are two functions: "dim" and "gexprOfExpr", and I can get only one of them to work right away. Am I trying to make it impossible?

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

Note. I know the type I'm trying to recover. If this helps, it will be fine:

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

Answer 1

Saizan from #haskell gave me a hint that led to an answer. Here's the working version:

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