kosmikus

{-# LANGUAGE DataKinds, GADTs, PatternSynonyms, PolyKinds, ScopedTypeVariables, TypeFamilies, ViewPatterns #-}
module SingNat where

import Unsafe.Coerce

data Nat = Z | S Nat

data family Sing (a :: k)

newtype instance Sing (a :: Nat) = SingNat Int

kosmikus

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}
module PatSynEx where

data NS (f :: k -> *) (xs :: [k]) = NS Int

kosmikus

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
module CustomShowEnum where

kosmikus

type family SExprExt (ext :: k1) (f :: k2)  = (r :: (* -> *)) | r -> ext where
  SExprExt ('[] :: [* -> *]) f = Union (MapList ('[] :: [* -> *]) f)
  SExprExt r                 f = Union (MapList r                 f)

class (Functor (SExprExt ext f), Foldable (SExprExt ext f), Traversable (SExprExt ext f)) =>  SimpleExprExtension ext f a where
  functorWitness :: p ext f a -> Dict (Functor (SExprExt ext f))
  functorWitness _ = Dict
  foldableWitness :: p ext f a -> Dict (Foldable (SExprExt ext f))
  foldableWitness _ = Dict
  traversableWitness :: p ext f a -> Dict (Traversable (SExprExt ext f))

kosmikus

Main.gshowP_$dAll :: All MyShow Any
[GblId,
 Unf=Unf{Src=<vanilla>, TopLvl=True, Value=False, ConLike=False,
         WorkFree=False, Expandable=True, Guidance=IF_ARGS [] 20 0}]
Main.gshowP_$dAll
  = ghc-prim-0.5.0.0:GHC.Classes.$p1(%,%)
      @ (All MyShow Any)
      @ (All (All MyShow) Any)
      (ghc-prim-0.5.0.0:GHC.Classes.C:(%%)
       `cast` (Sub (Sym (Main.D:R:AllFk_c[][0] <[*]>_N <All MyShow>_N))

kosmikus

{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE MultiParamTypeClasses, DataKinds, PolyKinds #-}
{-# LANGUAGE FlexibleInstances, TypeOperators, TypeFamilies #-}
{-# LANGUAGE ConstraintKinds, UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses, RankNTypes #-}
{-# LANGUAGE FlexibleContexts, ScopedTypeVariables #-}
{-# LANGUAGE AllowAmbiguousTypes, StandaloneDeriving #-}
module RecordDiff where

import Data.Functor.Identity

kosmikus

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# LANGUAGE PolyKinds #-}
module KindGenericSOP where

import Data.Kind
import Generics.SOP

kosmikus

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
module R where

import Data.Functor.Identity

kosmikus

instance {-# OVERLAPPING #-} (Validatable' r, KnownSymbol s) => Validatable' (MetaX s r) where
  form' = M1 <$> (fieldName DIG..: form')
    where
      fieldName = pack $ symbolVal (Proxy :: Proxy s)

instance {-# OVERLAPPABLE #-} (Validatable' r) => Validatable' (M1 i a r) where
  form' = M1 <$> form'

instance (Validatable' r, Validatable' s) => Validatable' (r :*: s) where
  form' = (:*:) <$> form' <*> form'

kosmikus

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RoleAnnotations #-}
module CoerceTest where

import Data.Coerce

type role A phantom
data A a = MkA Int

-- works (CORRECT)