noughtmare

{-# LANGUAGE GHC2021, TypeFamilies, TypeAbstractions, ImpredicativeTypes #-}
import Data.Kind
import Prelude hiding (id, (.), curry, fst, snd)

type (:->) :: forall ob. ob -> ob -> Type
type (:->) @ob = Hom' ob

class Category ob where
  type Hom' ob :: ob -> ob -> Type
  id :: Hom' ob a a

noughtmare

open import Data.List
open import Data.List.Membership.Propositional
open import Data.Nat
open import Data.Nat.Properties
open import Data.Product using (∃-syntax ; _,_)
open import Data.List.Relation.Unary.Any using (here ; there)
open import Relation.Binary.PropositionalEquality

variable A B : Set
         s r : ℕ

noughtmare

{-# LANGUAGE GHC2024 #-}

import System.IO
import Control.Monad
import Control.Applicative
import Data.ByteString (hGet, ByteString)

newtype M a = M { runM :: Handle -> Int -> IO (Maybe (Int, a)) } deriving Functor

instance Applicative M where

noughtmare

{-# LANGUAGE TypeApplications, TypeAbstractions #-}
module T where

import GHC.Base (build)
import Prelude hiding (Maybe)

data Stream a = forall s. MkStream (s -> Step s a) !s
data Step s a = Yield a !s | Done

toStream :: [a] -> Stream a

noughtmare

{-# LANGUAGE PatternSynonyms, ViewPatterns, DataKinds #-}
module SafeHoas (BuildExp, app, lam, MatchExp (Var, App, Lam), shift) where

import Data.Coerce

type Name = String

data Exp = Var' Name | App' Exp Exp | Lam' (Exp -> Exp)

newtype BuildExp (s :: ()) = BuildExp Exp

noughtmare

{-# LANGUAGE LambdaCase #-}
{-# OPTIONS_GHC -Wall -Wno-name-shadowing #-}
import Control.Monad (ap)

data Free f a = Pure a | Op (f (Free f a)) deriving Functor

-- We do not enforce that the end references must be used, so this can be used "unsafely" in
-- the sense that one or both of the scoped computations end with Pure and thus are not 
-- really scoped, but semantically that never changes the meaning. It only means that any
-- operations that occur afterwards may be duplicated.

noughtmare

open import Level using (Level) renaming (suc to lsuc ; zero to lzero)
open import Function
open import Data.Sum using (_⊎_ ; inj₁ ; inj₂)

variable ℓ : Level

data Desc (I : Set) : Set₁ where
  var : I → Desc I
  σ π : (A : Set) (D : A → Desc I) → Desc I
  _×D_ : Desc I → Desc I → Desc I

noughtmare

#!/usr/bin/env bash

# Use getopt to parse long options
OPTIONS=$(getopt -o '' --long numeric-version -o '' --long supported-languages -o '' --long info -o '' --long print-global-package-db -o '' --long print-libdir -- "$@" 2>/dev/null)
if [ $? -ne 0 ]; then
  echo HERE: fakeghc $@
  exit 0
fi

# Reorder the positional parameters according to getopt's output

noughtmare

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -Wall #-}
{-# LANGUAGE QuantifiedConstraints #-}

import Data.Kind
import Prelude hiding ((>>=), return, gcd)
import Data.Proxy

type CType = [Type] -> Type

noughtmare

open import Data.Fin as Fin using (Fin ; #_ ; _≟_)
open import Data.Fin.Properties using (suc-injective)
open import Level as Level using (Level)
open import Data.Unit using (⊤ ; tt)
open import Data.Empty
open import Data.Product as Product
open import Data.Product.Properties as Product using (,-injective ; ≡-dec)
open import Data.Sum
open import Relation.Binary.PropositionalEquality
open import Data.Nat using (ℕ ; _+_)