{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Language.Symantic.Type.Map where

import Data.Proxy
import Data.Map.Strict as Map

import Language.Symantic.Type.Root
import Language.Symantic.Type.Type0
import Language.Symantic.Type.Type2

-- * Type 'Type_Map'
-- | The 'Map' type.
type Type_Map = Type_Type2 (Proxy Map)

type instance Constraint2_of (Proxy Map)
 = Constraint2_Map

{- FIXME: Could not deduce (Ord k) arising from a pattern…
pattern Type_Map
 :: Ord k => root k -> root a
 -> Type_Type2 (Proxy Map) root (Map k a)
pattern Type_Map k a
 = Type_Type2 Proxy k a
-}

-- ** Class 'Constraint2_Map'
class Constraint2_Map k a
instance Ord k => Constraint2_Map k a

instance -- String_from_Type
 String_from_Type root =>
 String_from_Type (Type_Map root) where
	string_from_type (Type_Type2 _ k a) =
		"Map (" ++ string_from_type k ++ ")"
		 ++ " (" ++ string_from_type a ++ ")"

-- | Inject 'Type_Map' within a root type.
type_map
 :: forall root h_k h_a.
 (Lift_Type_Root Type_Map root, Ord h_k)
 => root h_k -> root h_a
 -> root (Map h_k h_a)
type_map k a = lift_type_root (Type_Type2 Proxy k a
	 ::Type_Map root (Map h_k h_a))