UnsaturatedMultiConstraint_polymorphic-matchability.hs

{-# LANGUAGE PolyKinds               #-}
{-# LANGUAGE DataKinds               #-}
{-# LANGUAGE GADTs                   #-}
{-# LANGUAGE RankNTypes              #-}
{-# LANGUAGE UnsaturatedTypeFamilies #-}
{-# LANGUAGE TypeOperators           #-}

module Main where

import           Data.Kind

{-
$ ./_build/stage1/bin/ghc -o unsaturated-poly ../PolyUnsaturatedMultiConstraint.hs
$ ./unsaturated-poly 
I can show it: [False,True,False]
I can eq it: True
I can only show it: [False,True,True,True]
-}
main :: IO ()
main = do
  useShowEq (Box [False, True, False])
  simpleBox (Box [False, True, True, True])

-- It's matchability-polymorphic
data Box (c :: Type ->{m} Constraint) where
  Box :: forall m (c :: Type ->{m} Constraint) 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)

simpleBox :: Box Show -> IO ()
simpleBox box = case box of
  Box x -> do
    putStrLn $ "I can only show it: " ++ show x

Without the matchability polymorphism (i.e. using a ~> instead), we get this type error:

../PolyUnsaturatedMultiConstraint.hs:48:18: error:
    * Expected kind `* ~> Constraint',
        but `Show' has kind `* -> Constraint'
    * In the first argument of `Box', namely `Show'
      In the type signature: simpleBox :: Box Show ~> IO ()

---

With just -XTypeFamilies we get this type error:

../PolyUnsaturatedMultiConstraint.hs:33:14: error:
    * The type family `MultiConstraint' should have 2 arguments, but has been given 1
      (Use UnsaturatedTypeFamilies to permit this)
    * In the type signature:
        useShowEq :: Box (MultiConstraint '[Show, Eq]) ~> IO ()

As I did this, I figured out that you can get this nice Box interface w/type families alone without -XUnsaturatedTypeFamilies too:

https://gist.github.com/ramirez7/bcca51360df273e4a7a5a682e28fd7fa