Problem with singletons

dependent.hs

import Data.Singletons.Decide                                                                                                                                                                                       
import Data.Singletons.TH                                                                                                                                                                                           
import Data.Kind                                                                                                                                                                                                    
                                                                                                                                                                                                                    
                                                                                                                                                                                                                    
$(singletons [d|                                                                                                                                                                                                    
    data EType = EList EType                                                                                                                                                                                        
               | EInt                                                                                                                                                                                               
        deriving (Eq, Show)                                                                                                                                                                                         
    |])                                                                                                                                                                                                             
                                                                                                                                                                                                                    
                                                                                                                                                                                                                    
data IsList :: EType -> * where                                                                                                                                                                                     
    IsList :: IsList (EList a)                                                                                                                                                                                      
                                                                                                                                                                                                                    
data ElemTypeOf:: EType -> EType -> * where                                                                                                                                                                         
    ElemTypeOf :: ElemTypeOf t (EList t)                                                                                                                                                                            
                                                                                                                                                                                                                    
isElemTypeOf :: SEType t1 -> SEType t2 -> Maybe (ElemTypeOf t1 t2)                                                                                                                                                  
isElemTypeOf t1 (SEList t2) = case t1 %~ t2 of                                                                                                                                                                      
                                Proved _ -> Just ElemTypeOf                                                                                                                                                         
                                _ -> Nothing                                                                                                                                                                        
isElemTypeOf _ _ = Nothing                                                                                                                                                                                          
                                  
-- errors

    • Could not deduce: t1 ~ n
      from the context: t2 ~ 'EList n
        bound by a pattern with constructor:
                   SEList :: forall (z_a8CG :: EType) (n_a8CH :: EType).
                             z_a8CG ~ 'EList n_a8CH =>
                             Sing n_a8CH -> Sing z_a8CG,
                 in an equation for ‘isElemTypeOf’
        at src/Main.hs:34:18-26
      ‘t1’ is a rigid type variable bound by
        the type signature for:
          isElemTypeOf :: forall (t1 :: EType) (t2 :: EType).
                          SEType t1 -> SEType t2 -> Maybe (ElemTypeOf t1 t2)
        at src/Main.hs:33:17
      ‘n’ is a rigid type variable bound by
        a pattern with constructor:
          SEList :: forall (z_a8CG :: EType) (n_a8CH :: EType).
                    z_a8CG ~ 'EList n_a8CH =>
                    Sing n_a8CH -> Sing z_a8CG,
        in an equation for ‘isElemTypeOf’
        at src/Main.hs:34:18
      Expected type: Maybe (ElemTypeOf t1 t2)
        Actual type: Maybe (ElemTypeOf t1 ('EList t1))
    • In the expression: Just ElemTypeOf
      In a case alternative: Proved _ -> Just ElemTypeOf
      In the expression:
        case t1 %~ t2 of {
          Proved _ -> Just ElemTypeOf
          _ -> Nothing }
    • Relevant bindings include
        t2 :: Sing n (bound at src/Main.hs:34:25)
        t1 :: SEType t1 (bound at src/Main.hs:34:14)
        isElemTypeOf :: SEType t1 -> SEType t2 -> Maybe (ElemTypeOf t1 t2)
          (bound at src/Main.hs:34:1)