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 <oleg.grenrus@iki.fi>
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

phadej

diff --git a/Control/Monad/Trans/Class.hs b/Control/Monad/Trans/Class.hs
index b92bc0e..d6028dc 100644
--- a/Control/Monad/Trans/Class.hs
+++ b/Control/Monad/Trans/Class.hs
@@ -5,6 +5,7 @@
 #if __GLASGOW_HASKELL__ >= 710
 {-# LANGUAGE AutoDeriveTypeable #-}
 #endif
+{-# LANGUAGE QuantifiedConstraints #-}
 -----------------------------------------------------------------------------