Skip to content

Instantly share code, notes, and snippets.

Avatar

Ryan Scott RyanGlScott

View GitHub Profile
View gist:2404f1cee58152e1dd483d5b37a5ab7d
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE NamedWildCards #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeApplications #-}
{-# OPTIONS_GHC -Wno-partial-type-signatures #-}
module Foo where
import Data.Kind
View TypeLevelGlambda.hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
-- | Requires GHC 8.8 or later
module TypeLevelGlambda where
@RyanGlScott
RyanGlScott / Bug.hs
Created Feb 13, 2019
Pattern synonym existential scoping weirdness
View Bug.hs
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Bug where
import Data.Kind
import Data.Proxy
data T = forall k (a :: k). MkT (Proxy a)
View gist:dba49db44881735c3476e8b2483e25d1
{-# LANGUAGE RankNTypes #-}
module Bug where
import Data.Functor.Identity
newtype T f = MkT { unT :: forall a. f a }
works1 :: T Identity -> T Identity
works1 (MkT x) = MkT x
@RyanGlScott
RyanGlScott / Foo.hs
Last active Jan 9, 2019
Can you implement `foo` without `coerce`?
View Foo.hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
module Foo where
import Data.Coerce
type family F a
newtype T1 = MkT1 (forall a. F a)
newtype T2 = MkT2 (forall a. F a)
@RyanGlScott
RyanGlScott / SubstRep1.hs
Last active Dec 11, 2018
How to derive a Generic instance using nothing but Generic1
View SubstRep1.hs
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module SubstRep1 where
@RyanGlScott
RyanGlScott / CTuples.hs
Last active May 16, 2019
Partially applicable constraint tuple type constructors
View CTuples.hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableInstances #-}
#if __GLASGOW_HASKELL__ >= 708 && __GLASGOW_HASKELL__ < 710
{-# LANGUAGE NullaryTypeClasses #-}
#endif
#if __GLASGOW_HASKELL__ >= 800
{-# LANGUAGE UndecidableSuperClasses #-}
@RyanGlScott
RyanGlScott / S.hs
Last active Nov 30, 2018
Conor McBride's S combinator in GHC
View S.hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE LiberalTypeSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module S where
import Data.Kind
@RyanGlScott
RyanGlScott / ElimNat.hs
Last active Nov 14, 2018
Type-level eliminators in GHC!
View ElimNat.hs
#!/usr/bin/env cabal
{- cabal:
build-depends: base >= 4.12
, singleton-nats >= 0.4.1
, singletons >= 2.5.1
-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ImpredicativeTypes #-}
@RyanGlScott
RyanGlScott / Foo.idr
Created Nov 7, 2018
Why doesn't this typecheck?
View Foo.idr
module Foo
%default total
interface C a where
T' : Type
T : (a : Type) -> C a => Type
T a = T' {a}
interface (C a, Show (T a)) => D a where