kosmikus

{-# LANGUAGE DataKinds, FlexibleContexts, TypeFamilies, TypeOperators #-}
module SOPTail where

import Data.SOP
import Data.SOP.Dict

test :: (All c ys, ys ~ (x : xs)) => Proxy x -> Proxy c -> Dict (All c) xs
test _ _ = Dict

kosmikus

{-# LANGUAGE DerivingVia, ScopedTypeVariables, StandaloneDeriving, TypeApplications, TypeFamilies #-}
module DataFamilyDerivingVia where

import Data.Coerce

data family Foo a

newtype ByBar a = ByBar a

class Baz a where

kosmikus

{-| This @lens@ tutorial targets Haskell beginners and assumes only basic
    familiarity with Haskell.  By the end of this tutorial you should:

    * understand what problems the @lens@ library solves,

    * know when it is appropriate to use the @lens@ library,

    * be proficient in the most common @lens@ idioms,

    * understand the drawbacks of using lenses, and:

kosmikus

{-# LANGUAGE DataKinds, PolyKinds, MultiParamTypeClasses, TypeFamilies, TypeOperators #-}
{-# LANGUAGE FlexibleInstances, FlexibleContexts, UndecidableInstances, ScopedTypeVariables #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE UndecidableSuperClasses, TypeApplications  #-}
{-# LANGUAGE ConstraintKinds #-}
module CurryNP4 where

import Data.Kind
import Generics.SOP
import GHC.Exts

kosmikus

{-# LANGUAGE TypeFamilies #-}
module TypeFamilies where

type family A (x :: *) :: * where
  A x = x

type family B (x :: *) :: * where
  A x = x -- note A, not B !!
  
-- ghc-8.6.1 accepts this program, whereas ghc-8.4.3 reports an error

kosmikus

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ScopedTypeVariables #-}

kosmikus

{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeFamilies #-}
module Person where

import Generics.SOP
import qualified GHC.Generics as GHC

data Person' f =

kosmikus

{-# LANGUAGE FlexibleContexts, MultiParamTypeClasses, GADTs, DefaultSignatures, DeriveAnyClass, StandaloneDeriving, ScopedTypeVariables, TypeApplications #-}
module Buildable where

import Generics.SOP
import Generics.SOP.Metadata

class Buildable a where
  build :: IO a
  default build :: (Generic a, HasDatatypeInfo a, All2 Buildable (Code a)) => IO a
  build = gbuild

kosmikus

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MonoLocalBinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
module EnumRead where

import Data.Char
import qualified Data.Map
import Generics.SOP

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