RyanGlScott

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

RyanGlScott

I've discovered something how to do something that GHC never intended you to be able to do, and I'm wondering if there's a way to abuse this to do interesting things.

It's known that you can express visible, dependent quantification at the kind level:

data A a :: a -> Type

λ> :kind A

RyanGlScott

#!/usr/bin/env cabal
{- cabal:
build-depends: base       >= 4.9
             , QuickCheck >= 2.12
             , sop-core   >= 0.4
-}

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}

RyanGlScott

{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module IdleThoughtsOnGADTsAsNewtypes where

RyanGlScott

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilyDependencies #-}

RyanGlScott

$ make test TEST="prog001 prog002 prog003 ghci.prog010 prog013 prog012 ghci.prog009 ghci025 ghci038 ghci057 T2182ghci ghci058 T6106 T8353 T9293 T10989 T13825-ghci print007 break009 break008 break026 T4029"
make -C ./tests test
make[1]: Entering directory `/home/rgscott/Software/ghc3/testsuite/tests'
PYTHON="python3" "python3" ../driver/runtests.py  -e "ghc_compiler_always_flags='-dcore-lint -dcmm-lint -no-user-package-db -rtsopts  -fno-warn-missed-specialisations -fshow-warning-groups -fdiagnostics-color=never -fno-diagnostics-show-caret -dno-debug-output'" -e config.compiler_debugged=False -e ghc_with_native_codegen=1 -e config.have_vanilla=True -e config.have_dynamic=True -e config.have_profiling=False -e ghc_with_threaded_rts=1 -e ghc_with_dynamic_rts=1 -e config.have_interp=True -e config.unregisterised=False -e config.have_gdb=True -e config.have_readelf=True -e config.ghc_dynamic_by_default=False -e config.ghc_dynamic=True -e ghc_with_smp=1 -e ghc_with_llvm=0 -e windows=False -e darwin=False -e config.i

RyanGlScott

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
-- | When your idea isn't even good enough for an @acme@ package...
module Data.Type.Phantom where

RyanGlScott

module Retrofunctor where

import Control.Applicative
import Control.Arrow
import Data.Bifunctor.Biff
import Data.Bifunctor.Clown
import Data.Bifunctor.Flip
import Data.Bifunctor.Joker
import Data.Bifunctor.Product
import Data.Bifunctor.Sum

RyanGlScott

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeInType #-}

RyanGlScott

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}