Lysxia

Inductive E : Type -> Type :=
| C : E bool.

Goal forall (c : E bool), c = C.
Proof.
  intro c.
Qed. (* ??? *)

Lysxia

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}

Lysxia

{-# LANGUAGE
    DataKinds,
    PolyKinds,
    TypeFamilies,
    TypeInType,
    TypeOperators,
    UndecidableInstances #-}

module EvalTF where

Lysxia

{-# LANGUAGE TypeFamilies, UndecidableInstances #-}

-- https://blog.poisson.chat/posts/2018-07-09-type-gadt.html

module UnMTL where

import Control.Monad.Trans.Reader
import Control.Monad.Trans.State
import Control.Monad.Trans.Except
import Data.Functor.Identity

Lysxia

-- Coercible not symmetric on GHC 8.0, 8.2, somehow fixed on 8.4

{-# LANGUAGE
    AllowAmbiguousTypes,
    FlexibleContexts,
    ScopedTypeVariables,
    TypeFamilies,
    TypeApplications
    #-}

Lysxia

{-# LANGUAGE
    DataKinds,
    PolyKinds,
    TypeFamilies,
    TypeFamilyDependencies,
    TypeOperators,
    UndecidableInstances #-}
module U where

import Generics.SOP

Lysxia

class Functors n s t a b where
  fmaps :: (a -> b) -> s -> t

instance {-# OVERLAPPING #-} (s ~ a, t ~ b) => Functors 0 s t a b where
  fmaps = id

instance (Functors (n-1) s t a b, fs ~ f s, ft ~ f t, Functor f) => Functors n fs ft a b where
  fmaps = fmap . fmaps @(n-1)

Lysxia

class Uncurry f ts r where
  uncurry_ :: f -> NP I ts -> r

instance Uncurry f xs r => Uncurry (t -> f) (t ': ts) r where
  uncurry_ f (a :* as) = uncurry_ (f a) as

instance (s ~ r) => Uncurry s '[] r where
  uncurry_ z Nil = z

Lysxia

{-# LANGUAGE
    DeriveFunctor,
    GeneralizedNewtypeDeriving,
    InstanceSigs,
    RankNTypes,
    ScopedTypeVariables,
    TypeApplications #-}

import Control.Applicative
import Control.Monad.Except

Lysxia

main :: IO ()
main = do
  if True
    then pure ()
    else do
  print 0