RyanGlScott

{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module SubstRep1 where

RyanGlScott

{-# 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

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE LiberalTypeSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module S where

import Data.Kind

RyanGlScott

#!/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

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