fork(2) download

copy

{-# LANGUAGE PolyKinds  #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
 
 
main = print "Hello"
 
-- type SomeSing :: * -> *
data SomeSing k where 
    SomeSing ::  Sing (a :: k) -> SomeSing k
 
data family Sing (a :: k)
 
class SingKind k where
  fromSing :: Sing (a :: k) -> k
  toSing   :: k -> SomeSing k
 
-----
 
data instance (Sing 'True)  = STrue
data instance (Sing 'False) = SFalse
 
instance SingKind Bool where
  fromSing s = case s of
    STrue  -> True
    SFalse -> False
 
  toSing b = case b of
    True  -> SomeSing STrue
    False -> SomeSing SFalse
 
 

[1 of 1] Compiling Main             ( prog.hs, prog.o )

prog.hs:26:5: error:
    • Couldn't match type ‘a’ with ‘'True’
      ‘a’ is a rigid type variable bound by
        the type signature for:
          fromSing :: forall (a :: Bool). Sing a -> Bool
        at prog.hs:25:3-10
      Expected type: Sing a
        Actual type: Sing 'True
    • In the pattern: STrue
      In a case alternative: STrue -> True
      In the expression:
        case s of
          STrue -> True
          SFalse -> False
    • Relevant bindings include
        s :: Sing a (bound at prog.hs:25:12)
        fromSing :: Sing a -> Bool (bound at prog.hs:25:3)
   |
26 |     STrue  -> True
   |     ^^^^^

Standard output is empty