UnsaturatedMultiConstraint_monomorphic-matchability.hs

{-# LANGUAGE AllowAmbiguousTypes     #-}
{-# LANGUAGE PolyKinds               #-}
{-# LANGUAGE ConstraintKinds         #-}
{-# LANGUAGE DataKinds               #-}
{-# LANGUAGE FlexibleInstances       #-}
{-# LANGUAGE GADTs                   #-}
{-# LANGUAGE KindSignatures          #-}
{-# LANGUAGE MultiParamTypeClasses   #-}
{-# LANGUAGE RankNTypes              #-}
{-# LANGUAGE ScopedTypeVariables     #-}
{-# LANGUAGE TypeApplications        #-}
{-# LANGUAGE UnsaturatedTypeFamilies #-}
{-# LANGUAGE TypeOperators           #-}

module Main where

import           Data.Kind

{-
$ ./_build/stage1/bin/ghc -o unsaturated-mono ../MonoUnsaturatedMultiConstraint.hs 
[1 of 1] Compiling Main             ( ../MonoUnsaturatedMultiConstraint.hs, ../MonoUnsaturatedMultiConstraint.o )
Linking unsaturated-mono ...
$ ./unsaturated-mono 
I can show it: [False,True,False]
I can eq it: True
-}
main :: IO ()
main = useShowEq (Box [False, True, False])

-- TODO: Matchability polymorphism
data Box (c :: Type ~> Constraint) where
  Box :: forall c x. c x => x -> Box c

type family MultiConstraint (xs :: [Type -> Constraint]) a :: Constraint where
  MultiConstraint '[] a = ()
  MultiConstraint (x ': xs) a = (x a, MultiConstraint xs a)

useShowEq :: Box (MultiConstraint '[Show, Eq]) -> IO ()
useShowEq box = case box of
  Box x -> do
      putStrLn $ "I can show it: " ++ show x
      putStrLn $ "I can eq it: " ++ show (x == x)