Icelandjack

data Kl_kind :: (Type -> Type) -> Type where
  Kl :: Type -> Kl_kind(m)
  
type family
  UnKl (kl :: Kl_kind m) = (res :: Type) | res m -> kl where
  UnKl (Kl a) = a

Icelandjack

Non-standard operators I use :) linked to from my twitter profile

I use kind synonyms

type T   = Type
type TT  = T -> T
type TTT = T -> TT
type C   = Constraint
type TC  = T -> C

Icelandjack

-- type Sig k = [k] -> Type
-- 
-- data AST :: Sig k -> Sig k where
--   Sym  :: dom a -> AST dom a
--   (:$) :: AST dom (a:as) -> AST dom '[a] -> AST dom as

singletons [d| data N = O | S N |]

infixr 5 :·
data Vec :: N -> Type -> Type where

Icelandjack

-- SYSTEM F
--   http://homepages.inf.ed.ac.uk/slindley/papers/embedding-f.pdf
-- 
-- Type-level lambdas
--   https://gist.github.com/AndrasKovacs/ac71371d0ca6e0995541e42cd3a3b0cf


{-# language TemplateHaskell, ScopedTypeVariables, RankNTypes,
             TypeFamilies, UndecidableInstances, DeriveFunctor, GADTs,
             TypeOperators, TypeApplications, AllowAmbiguousTypes,

Icelandjack

Solving Trac ticket #14832:

{-# Language QuantifiedConstraints, ScopedTypeVariables, TypeOperators, GADTs, FlexibleInstances, UndecidableInstances, ConstraintKinds, MultiParamTypeClasses, InstanceSigs, TypeApplications #-}

import Prelude hiding (id, (.))
import Control.Category
import Data.Coerce

data Dict c where

Icelandjack

For the Trac ticket #14860.

All these types are valid for h, but its principal type involves -XQuantifiedConstraints

{-# Language FlexibleInstances, MultiParamTypeClasses, GADTs, QuantifiedConstraints #-}

import Data.Kind

type family FB (a::Type) (b::Type) :: Type where

Icelandjack

-- Response to
--   https://gist.github.com/sjoerdvisscher/e8ed8ca8f3b6420b4aebe020b9e8e235
--   https://twitter.com/sjoerd_visscher/status/975375241932427265

{-# Language QuantifiedConstraints, TypeOperators, RankNTypes, GADTs, ConstraintKinds, MultiParamTypeClasses, FlexibleInstances, UndecidableInstances, PolyKinds, InstanceSigs #-}

import Data.Coerce

type f ~> g = forall x. f x -> g x

Icelandjack

{-# Language QuantifiedConstraints #-}
{-# Language GADTs #-}
{-# Language ConstraintKinds #-}
{-# Language MultiParamTypeClasses #-}
{-# Language UndecidableSuperClasses #-}
{-# Language FlexibleInstances #-}
{-# Language UndecidableInstances #-}
{-# Language AllowAmbiguousTypes #-}

data D c where

Icelandjack

https://twitter.com/phadej/status/958227051374350336

{-# Language QuantifiedConstraints #-}

class    (forall xx. Eq xx => Eq (f xx)) => Eq1 f
instance (forall xx. Eq xx => Eq (f xx)) => Eq1 f

newtype New s a = New a

Icelandjack

class ListLike f where
  nil  :: f a
  cons :: a -> f a -> f a
  (·)  :: f a -> f a -> f a

newtype LL a = LL (forall ff. ListLike ff => ff a)

instance ListLike LL where
 nil :: LL a