Isolated.hs

{-# LANGUAGE TypeOperators, GADTs, FlexibleContexts, DataKinds, RankNTypes, PolyKinds, TypeFamilies, MultiParamTypeClasses, UndecidableInstances, UndecidableSuperClasses, FlexibleInstances, ConstraintKinds, TypeApplications, EmptyCase, ScopedTypeVariables, PartialTypeSignatures, TemplateHaskell #-}
module Partition where

import Data.Coerce
import Data.Kind
import Data.Proxy

data NP (f :: k -> Type) (xs :: [k]) where
  Nil :: NP f '[]
  (:*) :: f x -> NP f xs -> NP f (x : xs)

infixr 5 :*

strictToPair :: forall f a b . NP f '[a, b] -> (f a, f b)
strictToPair np =
  case np of
    (fx :* fxs) ->
      case (fxs {- :: NP f '[b] -}) of
        (fy :* fys) ->
          (fx, fy)