AndrasKovacs

{-# language
  TypeInType, ScopedTypeVariables, RankNTypes,
  GADTs, TypeOperators, TypeApplications, BangPatterns
#-}

-- requires ghc-typelits-natnormalise
{-# options_ghc -fplugin GHC.TypeLits.Normalise #-}

{-|
Tested with ghc-8.4.3

AndrasKovacs

data Ty : Set where
  ι   : Ty
  _⇒_ : Ty → Ty → Ty
infixr 3 _⇒_

data Con : Set where
  ∙   : Con
  _▶_ : Con → Ty → Con
infixl 3 _▶_

AndrasKovacs

{-# language OverloadedStrings, UnicodeSyntax, LambdaCase,
             ViewPatterns, NoMonomorphismRestriction #-}
{-# options_ghc -fwarn-incomplete-patterns #-}

{- Minimal bidirectional dependent type checker with type-in-type. Related to Coquand's
   algorithm. #-}

import Prelude hiding (all)

AndrasKovacs

{-# language ScopedTypeVariables, RankNTypes, TypeFamilies,
             UndecidableInstances, GADTs, TypeOperators,
             TypeApplications, AllowAmbiguousTypes, TypeInType,
             StandaloneDeriving #-}

import Data.Kind

-- singletons
--------------------------------------------------------------------------------

AndrasKovacs

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

import Data.Singletons.TH -- singletons 2.4.1
import Data.Kind

-- some standard stuff for later examples' sake

AndrasKovacs

{-# OPTIONS --without-K #-}

{-
Below is an example of proving *everything* about the substitution calculus of a
simple TT with Bool.

The more challenging solution:
  - If substitutions are defined as lists of terms, then if you manage to
    prove that substitutions form a category, almost certainly you're done,
    since you can only prove this is you have all relevant lemmas.

AndrasKovacs

{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveFunctor #-}

import Data.Kind
import Data.Coerce

-- type synonyms
--------------------------------------------------------------------------------

AndrasKovacs

open import Algebra
open import Data.Bool
open import Data.Empty
open import Data.List
open import Data.List.Properties
open import Data.Nat
open import Data.Product
open import Data.Unit
open import Function

AndrasKovacs

{-# language
  RankNTypes, GADTs, TypeInType, LambdaCase, TypeApplications,
  TypeOperators, StandaloneDeriving, TupleSections, EmptyCase,
  ScopedTypeVariables, TypeFamilies, ConstraintKinds,
  FlexibleContexts, MultiParamTypeClasses, AllowAmbiguousTypes,
  FlexibleInstances, DeriveFunctor, UndecidableInstances,
  NoMonomorphismRestriction #-}

module EffInference where

AndrasKovacs

{-# OPTIONS --without-K #-}

open import Data.List
open import Data.Sum
open import Relation.Binary.PropositionalEquality

module _ (A : Set) where

  data _∈_ (a : A) : List A → Set where
    here  : ∀ {as} → a ∈ (a ∷ as)