nfrisby

{-# LANGUAGE PolyKinds, TypeFamilies, DataKinds, TypeOperators #-}

{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances,
 UndecidableInstances, FlexibleContexts #-} -- for the hacky bit

{-# LANGUAGE GADTs #-} -- just for an example

module CovariantN where

import GHC.Prim (Any) -- just for convenience

nfrisby

{-# LANGUAGE TypeFamilies, PolyKinds, ConstraintKinds, Rank2Types,
  ScopedTypeVariables #-}

{-# LANGUAGE FlexibleInstances, UndecidableInstances, MultiParamTypeClasses
  #-} -- only for examples

module Proposed.Data.Constraint.Forall
  (module Data.Constraint,
   Forall, Bottom, inst) where

nfrisby

{-# LANGUAGE RankNTypes, TypeFamilies, DataKinds, TypeOperators,
  ScopedTypeVariables, PolyKinds, ConstraintKinds, GADTs,
  MultiParamTypeClasses, FlexibleInstances, UndecidableInstances,
  FlexibleContexts #-}

module InductiveConstraints where

import GHC.Prim (Constraint)

nfrisby

{-# LANGUAGE TypeFamilies, TypeOperators, ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving, FlexibleContexts, UndecidableInstances #-}

module NewGDApp where

import GHC.Generics hiding ((:.:)) -- I'm proposing an alternative to @:.:@.



-- Only for representations of constructor arguments, ie the leaves of @:*:@.                                                                                        

nfrisby

-- naturals
data Nat = Z | S Nat

-- indexes in the type list
type family Nth (n :: Nat) (ts :: [k]) :: k
type instance Nth Z     (a ': as) = a
type instance Nth (S n) (a ': as) = Nth n as

-- represents an uncurried application of t
data family W (t :: k) :: [*] -> *

nfrisby

{-# LANGUAGE PolyKinds, GADTs, DataKinds, TypeFamilies, TypeOperators,
  MultiParamTypeClasses, FlexibleContexts, FlexibleInstances,
  UndecidableInstances #-}

-- this gist demonstrates some GHC 7.6 behaviors that I'm seeing as some type errors (example at the bottom).

module GHC_Query where

data Proxy (t :: k) = Proxy
data KindProxy (t :: *) = KindProxy  -- a type-level proxy for kinds