SHARE
TWEET

Untitled

a guest Apr 20th, 2019 128 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. {-# Language
  2.  DataKinds,
  3.  TypeOperators,
  4.  PolyKinds,
  5.  TypeFamilies,
  6.  UndecidableInstances,
  7.  GADTs,
  8.  RankNTypes
  9. #-}
  10.  
  11. data Nat = Z | S Nat
  12.            deriving (Show, Eq, Ord)
  13.  
  14. type family Elem (x :: a) (xs :: [a]) :: Bool where
  15.  Elem _ '[] = 'False
  16.  Elem x (x ': _) = 'True
  17.  Elem x (_ ': xs) = Elem x xs
  18.  
  19. type SumType (xs :: [*]) = forall x. True ~ (x `Elem` xs) => x
  20.  
  21. type Eg = [Bool,Int,Bool]
  22.  
  23. eg :: SumType Eg
  24. eg = False
  25.  
  26. {-
  27.  
  28.  
  29.    * Could not deduce: x ~ Bool
  30.      from the context: 'True ~ Elem x Eg
  31.         bound by the type signature for:
  32.                    eg :: SumType Eg
  33.       `x' is a rigid type variable bound by
  34.        the type signature for:
  35.          eg :: SumType Eg
  36.    * In the expression: False
  37.      In an equation for `eg': eg = False
  38.     * Relevant bindings include
  39.         eg :: x
  40.    |
  41.    | eg = False
  42.    |      ^^^^^
  43. -}
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand
 
Top