JakobBruenker

{-# LANGUAGE GeneralizedNewtypeDeriving, ViewPatterns, LambdaCase, MultiWayIf #-}

module Main where

import Control.Applicative
import Control.Monad.State
import Data.Bits
import Data.Maybe
import Data.Char
import Data.List

JakobBruenker

#include <Windows.h>
#include <stdlib.h>
#include <stdio.h>

// Take care to call the Bindings as extended Key Press if the keys have an
// extended scan code
const WORD const BINDINGS[21] = {
    0x11, // Move Forward
    0x1F, // Move Backward
    0x1E, // Strafe Left

JakobBruenker

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE DataKinds #-}
-- {-# LANGUAGE IncoherentInstances #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE AllowAmbiguousTypes #-}

JakobBruenker

{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}

module CompileTime where

JakobBruenker

{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE AllowAmbiguousTypes #-}

module LongTypeError where

import Data.Singletons.Prelude

JakobBruenker

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}

module ListOf where

-- was a closed type family at first, but jle` said it might be cleaner to put
-- it inside the class, and I agree

JakobBruenker

How.hs:24:13: error:
    • Could not deduce (Storable t0)
      from the context: Storable t
        bound by the type signature for:
                   method :: forall t. Storable t => Int
        at How.hs:24:13-44
      The type variable ‘t0’ is ambiguous
    • When checking that instance signature for ‘method’
        is more general than its signature in the class
        Instance sig: forall t. Storable t => Int

JakobBruenker

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE EmptyCase #-}

JakobBruenker

{-# OPTIONS_GHC -Wall -Wno-unticked-promoted-constructors #-}
{-# LANGUAGE Haskell2010
  , TypeFamilies
  , DataKinds
  , PolyKinds
  , RankNTypes
  , TypeOperators
  , TemplateHaskell
  , GADTs
  , ScopedTypeVariables

JakobBruenker

module TooLong where

open import Agda.Builtin.Nat renaming (Nat to ℕ)
open import Agda.Primitive
open import Agda.Builtin.Bool
open import Agda.Builtin.Equality

data SK : Set where
  S : SK
  K : SK