A file to demonstrate set-inclusion constraint issues in Haskell.

hlist-set-inclusion-issues.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE FlexibleContexts     #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}

module HList where

import Control.Monad.State (State, modify)

data HList xs where
  HNil :: HList '[]
  HCons :: x -> HList xs -> HList (x  ': xs)

class Elem (x :: *) (xs :: [*]) where
  getElem :: HList xs -> x

instance {-# OVERLAPPABLE #-}
  Elem x xs => Elem x (notIt ': xs) where
    getElem (HCons _ hTail) = getElem hTail

instance {-# OVERLAPPABLE #-}
  Elem x xs => Elem x (x ': xs) where
    getElem (HCons x _) = x

-- | this compiles
foo :: Elem a effects => HList effects -> a
foo = getElem

-- | this compiles: requires concrete types + scoped type variables
bar :: Elem (State Int Char) effects => HList effects -> (Int -> Int) -> State Int ()
bar effects manipulate =
  let (state :: State Int Char) = getElem effects
  in state >>= const (modify manipulate)

-- | will NOT compile
baz :: Elem (State s a) effects => HList effects -> (s -> s) -> State s ()
baz effects manipulate =
  let state = getElem effects
  in state >>= const (modify manipulate)

-- | will still NOT compile, even after adding scoping.
bazz :: Elem (State s a) effects => HList effects -> (s -> s) -> State s ()
bazz effects manipulate =
  let (state :: State s a) = getElem effects
  in state >>= const (modify manipulate)