phadej

Only in DBFunctor-0.1.2.1: cabal.project
Only in DBFunctor-0.1.2.1: dist-newstyle
Only in DBFunctor-0.1.2.1: .ghc.environment.x86_64-linux-8.6.5
diff -ur orig/DBFunctor-0.1.2.1/src/RTable/Core.hs DBFunctor-0.1.2.1/src/RTable/Core.hs
--- orig/DBFunctor-0.1.2.1/src/RTable/Core.hs	2021-05-23 18:03:12.000000000 +0300
+++ DBFunctor-0.1.2.1/src/RTable/Core.hs	2021-10-28 00:00:45.265149734 +0300
@@ -818,11 +818,6 @@
     -- anything else is just False
     _ == _ = False
 

phadej

{-# OPTIONS --cubical --type-in-type #-}
module Mokhov where

open import Cubical.Foundations.Everything
open import Cubical.Data.Sum
open import Cubical.Data.Prod
open import Cubical.Data.Unit

record Mokhov (F : Set → Set) (G : Set → Set) (A : Set) : Set where
  constructor mokhov

phadej

data Mokhov2 f g a where
    Mokhov2 :: (x -> Either a (y -> a)) -> f x -> g y -> Mokhov2 f g a

toMokhov2 :: Mokhov f g a -> Mokhov2 f g a
toMokhov2 (x :<*?: y) = Mokhov2 f y x where
    f ::  (x -> a) -> Either a (Either x a -> a)
    f xa = Right $ either xa id

fromMokhov2 :: (Functor f, Functor g) => Mokhov2 f g a -> Mokhov f g a
fromMokhov2 (Mokhov2 f x y) =

phadej

-- Selective
class Applicative f => Selective f where
    select :: f (Either a b) -> f (a -> b) -> f b

apS :: Selective f => f (a -> b) -> f a -> f b
apS f x = select (Left <$> f) ((&) <$> x)

-- Free Selective
data Select f a where
    Pure :: a -> Select f a

phadej

{-# LANGUAGE TypeFamilies, RankNTypes #-}

import Data.Kind
import Data.Coerce
import Data.Functor.Identity
import Data.Proxy
import Data.Void

-- from hkd package, for FFunctor
import Data.HKD

phadej

{-# LANGUAGE DataKinds, PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS -Wall -Wno-unticked-promoted-constructors #-}

import qualified Control.Category as C

-- It's all paths...

phadej

From 99908846a224e73ef7322604048dd21a22dbbcfb Mon Sep 17 00:00:00 2001
From: Oleg Grenrus <[email protected]>
Date: Fri, 16 Apr 2021 19:40:18 +0300
Subject: [PATCH] WIP: make basement,memory,cryptonite dependency optional

Few tests don't pass. I probably screwed something in Dhall.Crypto
(those functions don't have tests and it's all ByteStrings, so
 maybe I convert to wrong bytes somewhere).

cryptohash-sha256 needs base relaxation too,

phadej

{-# OPTIONS --cubical --safe #-}
module TrueFalse where

open import Cubical.Foundations.Everything
open import Cubical.Data.Bool

-- The following is basic stuff
true≡true : true ≡ true
true≡true = refl

phadej

curl -O https://raw.githubusercontent.com/haskell/cabal/725ca482d869e03be66bc845b39662ec0609bd99/release.py
curl -O http://oleg.fi/cabal-install-3.4.0.0-rc4/Cabal-3.4.0.0.tar.gz
curl -O http://oleg.fi/cabal-install-3.4.0.0-rc4/cabal-install-3.4.0.0.tar.gz
cat > SHA256SUMS <<EOF
47f95c62b6ec25900ff391fccdbcb46dd87efca6a83d8e80d7834a2cee9158bc  release.py
a1e9d803bf99c4989c82d63f6ae619740ece0282987dd3c8bae2fe158b85ed4c  Cabal-3.4.0.0.tar.gz
0499406c277bcaa431a0666d3e5ea171ee5bd7d66e6cf48ff275452d0723bb8b  cabal-install-3.4.0.0.tar.gz
EOF
sha256sum -c SHA256SUMS

phadej

diff --git a/Cabal/src/Distribution/FieldGrammar/Newtypes.hs b/Cabal/src/Distribution/FieldGrammar/Newtypes.hs
index 3f37b43eb..35a1e781c 100644
--- a/Cabal/src/Distribution/FieldGrammar/Newtypes.hs
+++ b/Cabal/src/Distribution/FieldGrammar/Newtypes.hs
@@ -250,7 +250,11 @@ newtype FilePathNT = FilePathNT { getFilePathNT :: String }
 instance Newtype String FilePathNT
 
 instance Parsec FilePathNT where
-    parsec = pack <$> parsecToken
+    parsec = do