haskell.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE StandaloneDeriving #-}

module Lib
  ( someFunc,
  )
where

import Data.Singletons

data K = K0 | K1

newtype T (k :: K) = T String

data SomeT = forall (k :: K). SomeT (Sing k) (T k)

--    * Couldn't match type `k1' with `k'
--      Expected: T k
--        Actual: T k1
--      `k1' is a rigid type variable bound by
--        a pattern with constructor:
--          SomeT :: forall (k :: K). Sing k -> T k -> SomeT,
--        in an equation for `=='
--        at src/Lib.hs:20:1-32
--      `k' is a rigid type variable bound by
--        a pattern with constructor:
--          SomeT :: forall (k :: K). Sing k -> T k -> SomeT,
--        in an equation for `=='
--        at src/Lib.hs:20:1-32
--    * In the second argument of `(==)', namely `b2'
--      In the second argument of `(&&)', namely `((a2 == b2))'
--      In the expression: ((a1 == b1)) && ((a2 == b2))
--      When typechecking the code for `=='
--        in a derived instance for `Eq SomeT':
--        To see the code I am typechecking, use -ddump-deriv
--    * Relevant bindings include
--        b2 :: T k1 (bound at src/Lib.hs:20:1)
--        b1 :: Sing k1 (bound at src/Lib.hs:20:1)
--        a2 :: T k (bound at src/Lib.hs:20:1)
--        a1 :: Sing k (bound at src/Lib.hs:20:1)
--   |
--20 | deriving stock instance Eq SomeT
--   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

deriving stock instance Eq SomeT

someFunc :: IO ()
someFunc = putStrLn "hello"