Patterns

patterns.hs

{-# LANGUAGE  PatternSynonyms
            , GADTs
            , TypeApplications
            , RankNTypes
            , ScopedTypeVariables 
            , ViewPatterns
#-}

-- GADT of possible types
data Type a where
  TInt :: Type Int

class ToType a where
  toType :: Type a

instance ToType Int where
  toType = TInt

-- some opaque type
data Expr a where
  EInt :: Expr Int

-- existential adding info of ToType dictionary
data SomeExpr where
  Expr :: ToType a => Expr a -> SomeExpr

-- explicit use of dictionary
typeof :: forall a. ToType a => Expr a -> Type a
typeof _ = toType @a


-- here something wrong happens
{-# COMPLETE (:::) #-}
--pattern (:::) :: ToType a => Expr a -> Type a -> SomeExpr
pattern expr ::: tt <- Expr expr@(typeof -> tt)
  where expr ::: _  = Expr expr

test :: (MonadFail m) => m String
test = do
  _e ::: t <- pure $ Expr EInt
  case t of
    TInt -> pure "int"

main :: IO ()
main = test >>= putStrLn