Main.hs

{-# language UndecidableInstances #-}
{-# language FunctionalDependencies #-}
{-# language MultiParamTypeClasses #-}
{-# language DataKinds #-}
{-# language FlexibleInstances #-}
{-# language ExistentialQuantification #-}
{-# language PolyKinds #-}
{-# language TypeOperators #-}

module Main where

main :: IO ()
main = pure ()

class Construct (element :: kind) (rest :: [kind]) (list :: [kind]) | list element -> rest, list rest -> element

instance Construct head tail (head ': tail) 
instance {-# overlappable #-} Construct element rest tail => Construct element (head ': rest) (head ': tail)

data OpenSum l = forall value. UnsafeOpenSum value

inject ::
  forall list element rest.
  Construct element rest list =>
  element ->
  OpenSum list
inject = UnsafeOpenSum

openSum :: OpenSum '[Char, Bool]
openSum = inject 'c'

-- /home/rednaz/Documents/haskell/maguire_open_sum/open-sum/app/Main.hs:30:11: error:
--     • Couldn't match type ‘Bool’ with ‘Char’
--         arising from a functional dependency between:
--           constraint ‘Construct Char '[Char] '[Char, Bool]’
--             arising from a use of ‘inject’
--           instance ‘Construct head tail (head : tail)’
--             at app/Main.hs:17:10-43
--     • In the expression: inject 'c'
--       In an equation for ‘openSum’: openSum = inject 'c'
--    |
-- 30 | openSum = inject 'c'
--    |           ^^^^^^^^^^

-- Is the primary purpose of functional dependencies not improving
-- type inference? In this case, it is deriving the wrong type for
-- `rest` although being uniquely determined by the functional
-- dependency and then complains that the derived type violates the
-- functional dependency. Where did you even get `'[Char]` from?