{-# LANGUAGE AllowAmbiguousTypes  #-}
{-# LANGUAGE ConstraintKinds      #-}
{-# LANGUAGE TemplateHaskell      #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE UndecidableInstances #-}

{-# OPTIONS_HADDOCK not-home #-}

module Polysemy.Internal.CustomErrors
  ( AmbiguousSend
  , WhenStuck
  , FirstOrder
  , UnhandledEffect
  , DefiningModule
  , DefiningModuleForEffect
  ) where

import Data.Kind
import Fcf
import GHC.TypeLits
import Polysemy.Internal.Kind
import Polysemy.Internal.CustomErrors.Redefined
import Type.Errors hiding (IfStuck, WhenStuck, UnlessStuck)


------------------------------------------------------------------------------
-- | The module this effect was originally defined in. This type family is used
-- only for providing better error messages.
--
-- Calls to 'Polysemy.Internal.TH.Effect.makeSem' will automatically give
-- instances of 'DefiningModule'.
type family DefiningModule (t :: k) :: Symbol

type family DefiningModuleForEffect (e :: k) :: Symbol where
  DefiningModuleForEffect (e a) = DefiningModuleForEffect e
  DefiningModuleForEffect e     = DefiningModule e


-- TODO(sandy): Put in type-errors
type ShowTypeBracketed t = 'Text "("
                     ':<>: 'ShowType t
                     ':<>: 'Text ")"


------------------------------------------------------------------------------
-- | The constructor of the effect row --- it's either completely polymorphic,
-- a nil, or a cons.
data EffectRowCtor = TyVarR | NilR | ConsR


------------------------------------------------------------------------------
-- | Given that @r@ isn't stuck, determine which constructor it has.
type family UnstuckRState (r :: EffectRow) :: EffectRowCtor where
  UnstuckRState '[]      = 'NilR
  UnstuckRState (_ ': _) = 'ConsR


------------------------------------------------------------------------------
-- | Put brackets around @r@ if it's a cons.
type family ShowRQuoted (rstate :: EffectRowCtor) (r :: EffectRow) :: ErrorMessage where
  ShowRQuoted 'TyVarR r = 'ShowType r
  ShowRQuoted 'NilR   r = 'ShowType r
  ShowRQuoted 'ConsR  r = ShowTypeBracketed r


type AmbigousEffectMessage (rstate :: EffectRowCtor)
                           (r :: EffectRow)
                           (e :: k)
                           (t :: Effect)
                           (vs :: [Type]) =
        ( 'Text "Ambiguous use of effect '"
    ':<>: 'ShowType e
    ':<>: 'Text "'"
    ':$$: 'Text "Possible fix:"
    ':$$: 'Text "  add (Member ("
    ':<>: 'ShowType t
    ':<>: 'Text ") "
    ':<>: ShowRQuoted rstate r
    ':<>: 'Text ") to the context of "
    ':$$: 'Text "    the type signature"
    ':$$: 'Text "If you already have the constraint you want, instead"
    ':$$: 'Text "  add a type application to specify"
    ':$$: 'Text "    "
    ':<>: PrettyPrintList vs
    ':<>: 'Text " directly, or activate polysemy-plugin which"
    ':$$: 'Text "      can usually infer the type correctly."
        )

type AmbiguousSend r e =
      (IfStuck r
        (AmbiguousSendError 'TyVarR r e)
        (Pure (AmbiguousSendError (UnstuckRState r) r e)))


type family AmbiguousSendError rstate r e where
  AmbiguousSendError rstate r (e a b c d f) =
    TypeError (AmbigousEffectMessage rstate r e (e a b c d f) '[a, b c d f])

  AmbiguousSendError rstate r (e a b c d) =
    TypeError (AmbigousEffectMessage rstate r e (e a b c d) '[a, b c d])

  AmbiguousSendError rstate r (e a b c) =
    TypeError (AmbigousEffectMessage rstate r e (e a b c) '[a, b c])

  AmbiguousSendError rstate r (e a b) =
    TypeError (AmbigousEffectMessage rstate r e (e a b) '[a, b])

  AmbiguousSendError rstate r (e a) =
    TypeError (AmbigousEffectMessage rstate r e (e a) '[a])

  AmbiguousSendError rstate r e =
    TypeError
        ( 'Text "Could not deduce: (Member "
    ':<>: 'ShowType e
    ':<>: 'Text " "
    ':<>: ShowRQuoted rstate r
    ':<>: 'Text ") "
    ':$$: 'Text "Fix:"
    ':$$: 'Text "  add (Member "
    ':<>: 'ShowType e
    ':<>: 'Text " "
    ':<>: 'ShowType r
    ':<>: 'Text ") to the context of"
    ':$$: 'Text "    the type signature"
        )


data FirstOrderErrorFcf :: k -> Symbol -> Exp Constraint
type instance Eval (FirstOrderErrorFcf e fn) = $(te[t|
    UnlessPhantom
        (e PHANTOM)
        ( 'Text "'"
    ':<>: 'ShowType e
    ':<>: 'Text "' is higher-order, but '"
    ':<>: 'Text fn
    ':<>: 'Text "' can help only"
    ':$$: 'Text "with first-order effects."
    ':$$: 'Text "Fix:"
    ':$$: 'Text "  use '"
    ':<>: 'Text fn
    ':<>: 'Text "H' instead."
        ) |])

------------------------------------------------------------------------------
-- | This constraint gives helpful error messages if you attempt to use a
-- first-order combinator with a higher-order type.
type FirstOrder (e :: Effect) fn = UnlessStuck e (FirstOrderErrorFcf e fn)


------------------------------------------------------------------------------
-- | Unhandled effects
type UnhandledEffectMsg e
      = 'Text "Unhandled effect '"
  ':<>: 'ShowType e
  ':<>: 'Text "'"
  ':$$: 'Text "Probable fix:"
  ':$$: 'Text "  add an interpretation for '"
  ':<>: 'ShowType e
  ':<>: 'Text "'"

type CheckDocumentation e
      = 'Text "  If you are looking for inspiration, try consulting"
  ':$$: 'Text "    the documentation for module '"
  ':<>: 'Text (DefiningModuleForEffect e)
  ':<>: 'Text "'"

type family UnhandledEffect e where
  UnhandledEffect e =
    IfStuck (DefiningModule e)
            (TypeError (UnhandledEffectMsg e))
            (DoError (UnhandledEffectMsg e ':$$: CheckDocumentation e))


data DoError :: ErrorMessage -> Exp k
type instance Eval (DoError a) = TypeError a