{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE ViewPatterns               #-}
{-# LANGUAGE CPP                        #-}

------------------------------------------------------------------------------
-- The MIT License (MIT)
--
-- Copyright (c) 2017 Luka Horvat, 2019 Sandy Maguire
--
-- Permission is hereby granted, free of charge, to any person obtaining a copy
-- of this software and associated documentation files (the "Software"), to
-- deal in the Software without restriction, including without limitation the
-- rights to use, copy, modify, merge, publish, distribute, sublicense, and/or
-- sell copies of the Software, and to permit persons to whom the Software is
-- furnished to do so, subject to the following conditions:
--
-- The above copyright notice and this permission notice shall be included in
-- all copies or substantial portions of the Software.
--
-- THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
-- IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
-- FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
-- AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
-- LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
-- FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS
-- IN THE SOFTWARE.
--
------------------------------------------------------------------------------
--
-- This module was originally based on 'Control.Effects.Plugin' from the
-- 'simple-effects' package, by Luka Horvat.
--
-- https://gitlab.com/LukaHorvat/simple-effects/commit/966ce80b8b5777a4bd8f87ffd443f5fa80cc8845#f51c1641c95dfaa4827f641013f8017e8cd02aab

module Polysemy.Plugin.Fundep (fundepPlugin) where

import           Control.Monad
import           Data.Bifunctor
import           Data.Coerce
import           Data.IORef
import qualified Data.Map as M
import           Data.Maybe
import qualified Data.Set as S
import           Polysemy.Plugin.Fundep.Stuff
import           Polysemy.Plugin.Fundep.Unification
import           Polysemy.Plugin.Fundep.Utils
import           TcEvidence
import           TcPluginM (TcPluginM, tcPluginIO)
import           TcRnTypes
#if __GLASGOW_HASKELL__ >= 810
import           Constraint
#endif
import           TcSMonad hiding (tcLookupClass)
import           Type



fundepPlugin :: TcPlugin
fundepPlugin :: TcPlugin
fundepPlugin = TcPlugin :: forall s.
TcPluginM s
-> (s -> TcPluginSolver) -> (s -> TcPluginM ()) -> TcPlugin
TcPlugin
  { tcPluginInit :: TcPluginM (IORef (Set Unification), PolysemyStuff 'Things)
tcPluginInit =
      (,) (IORef (Set Unification)
 -> PolysemyStuff 'Things
 -> (IORef (Set Unification), PolysemyStuff 'Things))
-> TcPluginM (IORef (Set Unification))
-> TcPluginM
     (PolysemyStuff 'Things
      -> (IORef (Set Unification), PolysemyStuff 'Things))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO (IORef (Set Unification)) -> TcPluginM (IORef (Set Unification))
forall a. IO a -> TcPluginM a
tcPluginIO (Set Unification -> IO (IORef (Set Unification))
forall a. a -> IO (IORef a)
newIORef Set Unification
forall a. Set a
S.empty)
          TcPluginM
  (PolysemyStuff 'Things
   -> (IORef (Set Unification), PolysemyStuff 'Things))
-> TcPluginM (PolysemyStuff 'Things)
-> TcPluginM (IORef (Set Unification), PolysemyStuff 'Things)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TcPluginM (PolysemyStuff 'Things)
polysemyStuff
  , tcPluginSolve :: (IORef (Set Unification), PolysemyStuff 'Things) -> TcPluginSolver
tcPluginSolve = (IORef (Set Unification), PolysemyStuff 'Things) -> TcPluginSolver
solveFundep
  , tcPluginStop :: (IORef (Set Unification), PolysemyStuff 'Things) -> TcPluginM ()
tcPluginStop = TcPluginM ()
-> (IORef (Set Unification), PolysemyStuff 'Things) -> TcPluginM ()
forall a b. a -> b -> a
const (TcPluginM ()
 -> (IORef (Set Unification), PolysemyStuff 'Things)
 -> TcPluginM ())
-> TcPluginM ()
-> (IORef (Set Unification), PolysemyStuff 'Things)
-> TcPluginM ()
forall a b. (a -> b) -> a -> b
$ () -> TcPluginM ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  }


------------------------------------------------------------------------------
-- | Corresponds to a 'Polysemy.Internal.Union.Find' constraint. For example,
-- given @Member (State s) r@, we would get:
data FindConstraint = FindConstraint
  { FindConstraint -> CtLoc
fcLoc        :: CtLoc
  , FindConstraint -> Type
fcEffectName :: Type  -- ^ @State@
  , FindConstraint -> Type
fcEffect     :: Type  -- ^ @State s@
  , FindConstraint -> Type
fcRow        :: Type  -- ^ @r@
  }


------------------------------------------------------------------------------
-- | Given a list of constraints, filter out the 'FindConstraint's.
getFindConstraints :: PolysemyStuff 'Things -> [Ct] -> [FindConstraint]
getFindConstraints :: PolysemyStuff 'Things -> [Ct] -> [FindConstraint]
getFindConstraints (PolysemyStuff 'Things -> ThingOf 'Things Class
forall (l :: LookupState). PolysemyStuff l -> ThingOf l Class
findClass -> ThingOf 'Things Class
cls) [Ct]
cts = do
  cd :: Ct
cd@CDictCan{cc_class :: Ct -> Class
cc_class = Class
cls', cc_tyargs :: Ct -> [Type]
cc_tyargs = [Type
_, Type
eff, Type
r]} <- [Ct]
cts
  Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> [()]) -> Bool -> [()]
forall a b. (a -> b) -> a -> b
$ Class
ThingOf 'Things Class
cls Class -> Class -> Bool
forall a. Eq a => a -> a -> Bool
== Class
cls'
  FindConstraint -> [FindConstraint]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (FindConstraint -> [FindConstraint])
-> FindConstraint -> [FindConstraint]
forall a b. (a -> b) -> a -> b
$ FindConstraint :: CtLoc -> Type -> Type -> Type -> FindConstraint
FindConstraint
    { fcLoc :: CtLoc
fcLoc = Ct -> CtLoc
ctLoc Ct
cd
    , fcEffectName :: Type
fcEffectName = Type -> Type
getEffName Type
eff
    , fcEffect :: Type
fcEffect = Type
eff
    , fcRow :: Type
fcRow = Type
r
    }


------------------------------------------------------------------------------
-- | If there's only a single @Member@ in the same @r@ whose effect name
-- matches and could possibly unify, return its effect (including tyvars.)
findMatchingEffectIfSingular
    :: FindConstraint
    -> [FindConstraint]
    -> Maybe Type
findMatchingEffectIfSingular :: FindConstraint -> [FindConstraint] -> Maybe Type
findMatchingEffectIfSingular (FindConstraint CtLoc
_ Type
eff_name Type
wanted Type
r) [FindConstraint]
ts =
  [Type] -> Maybe Type
forall a. [a] -> Maybe a
singleListToJust ([Type] -> Maybe Type) -> [Type] -> Maybe Type
forall a b. (a -> b) -> a -> b
$ do
    FindConstraint CtLoc
_ Type
eff_name' Type
eff' Type
r' <- [FindConstraint]
ts
    Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> [()]) -> Bool -> [()]
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Bool
eqType Type
eff_name Type
eff_name'
    Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> [()]) -> Bool -> [()]
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Bool
eqType Type
r Type
r'
    Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> [()]) -> Bool -> [()]
forall a b. (a -> b) -> a -> b
$ SolveContext -> Type -> Type -> Bool
canUnifyRecursive SolveContext
FunctionDef Type
wanted Type
eff'
    Type -> [Type]
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
eff'


------------------------------------------------------------------------------
-- | Given an effect, compute its effect name.
getEffName :: Type -> Type
getEffName :: Type -> Type
getEffName Type
t = (Type, [Type]) -> Type
forall a b. (a, b) -> a
fst ((Type, [Type]) -> Type) -> (Type, [Type]) -> Type
forall a b. (a -> b) -> a -> b
$ Type -> (Type, [Type])
splitAppTys Type
t


------------------------------------------------------------------------------
-- | Generate a wanted unification for the effect described by the
-- 'FindConstraint' and the given effect.
mkWantedForce
  :: FindConstraint
  -> Type
  -> TcPluginM (Unification, Ct)
mkWantedForce :: FindConstraint -> Type -> TcPluginM (Unification, Ct)
mkWantedForce FindConstraint
fc Type
given = do
  (CtEvidence
ev, Coercion
_) <- TcM (CtEvidence, Coercion) -> TcPluginM (CtEvidence, Coercion)
forall a. TcM a -> TcPluginM a
unsafeTcPluginTcM
           (TcM (CtEvidence, Coercion) -> TcPluginM (CtEvidence, Coercion))
-> (TcS (CtEvidence, Coercion) -> TcM (CtEvidence, Coercion))
-> TcS (CtEvidence, Coercion)
-> TcPluginM (CtEvidence, Coercion)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcS (CtEvidence, Coercion) -> TcM (CtEvidence, Coercion)
forall a. TcS a -> TcM a
runTcSDeriveds
           (TcS (CtEvidence, Coercion) -> TcPluginM (CtEvidence, Coercion))
-> TcS (CtEvidence, Coercion) -> TcPluginM (CtEvidence, Coercion)
forall a b. (a -> b) -> a -> b
$ CtLoc -> Role -> Type -> Type -> TcS (CtEvidence, Coercion)
newWantedEq (FindConstraint -> CtLoc
fcLoc FindConstraint
fc) Role
Nominal Type
wanted Type
given
  (Unification, Ct) -> TcPluginM (Unification, Ct)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( OrdType -> OrdType -> Unification
Unification (Type -> OrdType
OrdType Type
wanted) (Type -> OrdType
OrdType Type
given)
       , CtEvidence -> Ct
CNonCanonical CtEvidence
ev
       )
  where
    wanted :: Type
wanted = FindConstraint -> Type
fcEffect FindConstraint
fc

------------------------------------------------------------------------------
-- | Generate a wanted unification for the effect described by the
-- 'FindConstraint' and the given effect --- if they can be unified in this
-- context.
mkWanted
    :: FindConstraint
    -> SolveContext
    -> Type  -- ^ The given effect.
    -> TcPluginM (Maybe (Unification, Ct))
mkWanted :: FindConstraint
-> SolveContext -> Type -> TcPluginM (Maybe (Unification, Ct))
mkWanted FindConstraint
fc SolveContext
solve_ctx Type
given =
  Bool
-> TcPluginM (Unification, Ct)
-> TcPluginM (Maybe (Unification, Ct))
forall (m :: * -> *) (z :: * -> *) a.
(Monad m, Alternative z) =>
Bool -> m a -> m (z a)
whenA (Bool -> Bool
not (SolveContext -> Bool
mustUnify SolveContext
solve_ctx) Bool -> Bool -> Bool
|| SolveContext -> Type -> Type -> Bool
canUnifyRecursive SolveContext
solve_ctx Type
wanted Type
given) (TcPluginM (Unification, Ct)
 -> TcPluginM (Maybe (Unification, Ct)))
-> TcPluginM (Unification, Ct)
-> TcPluginM (Maybe (Unification, Ct))
forall a b. (a -> b) -> a -> b
$
    FindConstraint -> Type -> TcPluginM (Unification, Ct)
mkWantedForce FindConstraint
fc Type
given
  where
    wanted :: Type
wanted = FindConstraint -> Type
fcEffect FindConstraint
fc


------------------------------------------------------------------------------
-- | Given a list of 'Ct's, find any that are of the form
-- @[Irred] Sem r a ~ Something@, and return their @r@s.
getBogusRs :: PolysemyStuff 'Things -> [Ct] -> [Type]
getBogusRs :: PolysemyStuff 'Things -> [Ct] -> [Type]
getBogusRs PolysemyStuff 'Things
stuff [Ct]
wanteds = do
  CIrredCan CtEvidence
ct Bool
_ <- [Ct]
wanteds
  (Type
_, [Type
_, Type
_, Type
a, Type
b]) <- (Type, [Type]) -> [(Type, [Type])]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Type, [Type]) -> [(Type, [Type])])
-> (Type -> (Type, [Type])) -> Type -> [(Type, [Type])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> (Type, [Type])
splitAppTys (Type -> [(Type, [Type])]) -> Type -> [(Type, [Type])]
forall a b. (a -> b) -> a -> b
$ CtEvidence -> Type
ctev_pred CtEvidence
ct
  Maybe Type -> [Type]
forall a. Maybe a -> [a]
maybeToList (PolysemyStuff 'Things -> Type -> Maybe Type
extractRowFromSem PolysemyStuff 'Things
stuff Type
a)
    [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ Maybe Type -> [Type]
forall a. Maybe a -> [a]
maybeToList (PolysemyStuff 'Things -> Type -> Maybe Type
extractRowFromSem PolysemyStuff 'Things
stuff Type
b)


------------------------------------------------------------------------------
-- | Take the @r@ out of @Sem r a@.
extractRowFromSem :: PolysemyStuff 'Things -> Type -> Maybe Type
extractRowFromSem :: PolysemyStuff 'Things -> Type -> Maybe Type
extractRowFromSem (PolysemyStuff 'Things -> ThingOf 'Things TyCon
forall (l :: LookupState). PolysemyStuff l -> ThingOf l TyCon
semTyCon -> ThingOf 'Things TyCon
sem) Type
ty = do
  (TyCon
tycon, [Type
r, Type
_]) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty
  Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ TyCon
tycon TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
ThingOf 'Things TyCon
sem
  Type -> Maybe Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
r


------------------------------------------------------------------------------
-- | Given a list of bogus @r@s, and the wanted constraints, produce bogus
-- evidence terms that will prevent @IfStuck (LocateEffect _ r) _ _@ error messsages.
solveBogusError :: PolysemyStuff 'Things -> [Ct] -> [(EvTerm, Ct)]
solveBogusError :: PolysemyStuff 'Things -> [Ct] -> [(EvTerm, Ct)]
solveBogusError PolysemyStuff 'Things
stuff [Ct]
wanteds = do
  let splitTyConApp_list :: Type -> [(TyCon, [Type])]
splitTyConApp_list = Maybe (TyCon, [Type]) -> [(TyCon, [Type])]
forall a. Maybe a -> [a]
maybeToList  (Maybe (TyCon, [Type]) -> [(TyCon, [Type])])
-> (Type -> Maybe (TyCon, [Type])) -> Type -> [(TyCon, [Type])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe

  let bogus :: [Type]
bogus = PolysemyStuff 'Things -> [Ct] -> [Type]
getBogusRs PolysemyStuff 'Things
stuff [Ct]
wanteds
  ct :: Ct
ct@(CIrredCan CtEvidence
ce Bool
_) <- [Ct]
wanteds
  (TyCon
stuck, [Type
_, Type
_, Type
expr, Type
_, Type
_]) <- Type -> [(TyCon, [Type])]
splitTyConApp_list (Type -> [(TyCon, [Type])]) -> Type -> [(TyCon, [Type])]
forall a b. (a -> b) -> a -> b
$ CtEvidence -> Type
ctev_pred CtEvidence
ce
  Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> [()]) -> Bool -> [()]
forall a b. (a -> b) -> a -> b
$ TyCon
stuck TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== PolysemyStuff 'Things -> ThingOf 'Things TyCon
forall (l :: LookupState). PolysemyStuff l -> ThingOf l TyCon
ifStuckTyCon PolysemyStuff 'Things
stuff
  (TyCon
idx, [Type
_, Type
_, Type
r]) <- Type -> [(TyCon, [Type])]
splitTyConApp_list Type
expr
  Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> [()]) -> Bool -> [()]
forall a b. (a -> b) -> a -> b
$ TyCon
idx TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== PolysemyStuff 'Things -> ThingOf 'Things TyCon
forall (l :: LookupState). PolysemyStuff l -> ThingOf l TyCon
locateEffectTyCon PolysemyStuff 'Things
stuff
  Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> [()]) -> Bool -> [()]
forall a b. (a -> b) -> a -> b
$ OrdType -> [OrdType] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem @[] (Type -> OrdType
OrdType Type
r) ([OrdType] -> Bool) -> [OrdType] -> Bool
forall a b. (a -> b) -> a -> b
$ [Type] -> [OrdType]
coerce [Type]
bogus
  (EvTerm, Ct) -> [(EvTerm, Ct)]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Char] -> EvTerm
forall a. HasCallStack => [Char] -> a
error [Char]
"bogus proof for stuck type family", Ct
ct)


------------------------------------------------------------------------------
-- | Determine if there is exactly one wanted find for the @r@ in question.
exactlyOneWantedForR
    :: [FindConstraint]  -- ^ Wanted finds
    -> Type              -- ^ Effect row
    -> Bool
exactlyOneWantedForR :: [FindConstraint] -> Type -> Bool
exactlyOneWantedForR [FindConstraint]
wanteds
    = Bool -> Maybe Bool -> Bool
forall a. a -> Maybe a -> a
fromMaybe Bool
False
    (Maybe Bool -> Bool) -> (Type -> Maybe Bool) -> Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (OrdType -> Map OrdType Bool -> Maybe Bool)
-> Map OrdType Bool -> OrdType -> Maybe Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip OrdType -> Map OrdType Bool -> Maybe Bool
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Map OrdType Bool
singular_r
    (OrdType -> Maybe Bool) -> (Type -> OrdType) -> Type -> Maybe Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> OrdType
OrdType
  where
    singular_r :: Map OrdType Bool
singular_r = [(OrdType, Bool)] -> Map OrdType Bool
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList
               -- TODO(sandy): Nothing fails if this is just @second (const
               -- True)@. Why not? Incomplete test suite, or doing too much
               -- work?
               ([(OrdType, Bool)] -> Map OrdType Bool)
-> ([OrdType] -> [(OrdType, Bool)])
-> [OrdType]
-> Map OrdType Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((OrdType, Int) -> (OrdType, Bool))
-> [(OrdType, Int)] -> [(OrdType, Bool)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Int -> Bool) -> (OrdType, Int) -> (OrdType, Bool)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
1))
               ([(OrdType, Int)] -> [(OrdType, Bool)])
-> ([OrdType] -> [(OrdType, Int)])
-> [OrdType]
-> [(OrdType, Bool)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [OrdType] -> [(OrdType, Int)]
forall a. Eq a => [a] -> [(a, Int)]
countLength
               ([OrdType] -> Map OrdType Bool) -> [OrdType] -> Map OrdType Bool
forall a b. (a -> b) -> a -> b
$ Type -> OrdType
OrdType (Type -> OrdType)
-> (FindConstraint -> Type) -> FindConstraint -> OrdType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FindConstraint -> Type
fcRow (FindConstraint -> OrdType) -> [FindConstraint] -> [OrdType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [FindConstraint]
wanteds


solveFundep
    :: ( IORef (S.Set Unification)
       , PolysemyStuff 'Things
       )
    -> [Ct]
    -> [Ct]
    -> [Ct]
    -> TcPluginM TcPluginResult
solveFundep :: (IORef (Set Unification), PolysemyStuff 'Things) -> TcPluginSolver
solveFundep (IORef (Set Unification), PolysemyStuff 'Things)
_ [Ct]
_ [Ct]
_ [] = TcPluginResult -> TcPluginM TcPluginResult
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TcPluginResult -> TcPluginM TcPluginResult)
-> TcPluginResult -> TcPluginM TcPluginResult
forall a b. (a -> b) -> a -> b
$ [(EvTerm, Ct)] -> [Ct] -> TcPluginResult
TcPluginOk [] []
solveFundep (IORef (Set Unification)
ref, PolysemyStuff 'Things
stuff) [Ct]
given [Ct]
_ [Ct]
wanted = do
  let wanted_finds :: [FindConstraint]
wanted_finds = PolysemyStuff 'Things -> [Ct] -> [FindConstraint]
getFindConstraints PolysemyStuff 'Things
stuff [Ct]
wanted
      given_finds :: [FindConstraint]
given_finds  = PolysemyStuff 'Things -> [Ct] -> [FindConstraint]
getFindConstraints PolysemyStuff 'Things
stuff [Ct]
given

  [Maybe (Unification, Ct)]
eqs <- [FindConstraint]
-> (FindConstraint -> TcPluginM (Maybe (Unification, Ct)))
-> TcPluginM [Maybe (Unification, Ct)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [FindConstraint]
wanted_finds ((FindConstraint -> TcPluginM (Maybe (Unification, Ct)))
 -> TcPluginM [Maybe (Unification, Ct)])
-> (FindConstraint -> TcPluginM (Maybe (Unification, Ct)))
-> TcPluginM [Maybe (Unification, Ct)]
forall a b. (a -> b) -> a -> b
$ \FindConstraint
fc -> do
    let r :: Type
r  = FindConstraint -> Type
fcRow FindConstraint
fc
    case FindConstraint -> [FindConstraint] -> Maybe Type
findMatchingEffectIfSingular FindConstraint
fc [FindConstraint]
given_finds of
      -- We found a real given, therefore we are in the context of a function
      -- with an explicit @Member e r@ constraint. We also know it can
      -- be unified (although it may generate unsatisfiable constraints).
      Just Type
eff' -> (Unification, Ct) -> Maybe (Unification, Ct)
forall a. a -> Maybe a
Just ((Unification, Ct) -> Maybe (Unification, Ct))
-> TcPluginM (Unification, Ct)
-> TcPluginM (Maybe (Unification, Ct))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FindConstraint -> Type -> TcPluginM (Unification, Ct)
mkWantedForce FindConstraint
fc Type
eff'

      -- Otherwise, check to see if @r ~ (e ': r')@. If so, pretend we're
      -- trying to solve a given @Member e r@. But this can only happen in the
      -- context of an interpreter!
      Maybe Type
Nothing ->
        case Type -> (Type, [Type])
splitAppTys Type
r of
          (Type
_, [Type
_, Type
eff', Type
_]) ->
            FindConstraint
-> SolveContext -> Type -> TcPluginM (Maybe (Unification, Ct))
mkWanted FindConstraint
fc
                     (Bool -> SolveContext
InterpreterUse (Bool -> SolveContext) -> Bool -> SolveContext
forall a b. (a -> b) -> a -> b
$ [FindConstraint] -> Type -> Bool
exactlyOneWantedForR [FindConstraint]
wanted_finds Type
r)
                     Type
eff'
          (Type, [Type])
_ -> Maybe (Unification, Ct) -> TcPluginM (Maybe (Unification, Ct))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Unification, Ct)
forall a. Maybe a
Nothing

  -- We only want to emit a unification wanted once, otherwise a type error can
  -- force the type checker to loop forever.
  Set Unification
already_emitted <- IO (Set Unification) -> TcPluginM (Set Unification)
forall a. IO a -> TcPluginM a
tcPluginIO (IO (Set Unification) -> TcPluginM (Set Unification))
-> IO (Set Unification) -> TcPluginM (Set Unification)
forall a b. (a -> b) -> a -> b
$ IORef (Set Unification) -> IO (Set Unification)
forall a. IORef a -> IO a
readIORef IORef (Set Unification)
ref
  let ([Unification]
unifications, [Ct]
new_wanteds) = Set Unification -> [(Unification, Ct)] -> ([Unification], [Ct])
unzipNewWanteds Set Unification
already_emitted ([(Unification, Ct)] -> ([Unification], [Ct]))
-> [(Unification, Ct)] -> ([Unification], [Ct])
forall a b. (a -> b) -> a -> b
$ [Maybe (Unification, Ct)] -> [(Unification, Ct)]
forall a. [Maybe a] -> [a]
catMaybes [Maybe (Unification, Ct)]
eqs
  IO () -> TcPluginM ()
forall a. IO a -> TcPluginM a
tcPluginIO (IO () -> TcPluginM ()) -> IO () -> TcPluginM ()
forall a b. (a -> b) -> a -> b
$ IORef (Set Unification)
-> (Set Unification -> Set Unification) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef (Set Unification)
ref ((Set Unification -> Set Unification) -> IO ())
-> (Set Unification -> Set Unification) -> IO ()
forall a b. (a -> b) -> a -> b
$ Set Unification -> Set Unification -> Set Unification
forall a. Ord a => Set a -> Set a -> Set a
S.union (Set Unification -> Set Unification -> Set Unification)
-> Set Unification -> Set Unification -> Set Unification
forall a b. (a -> b) -> a -> b
$ [Unification] -> Set Unification
forall a. Ord a => [a] -> Set a
S.fromList [Unification]
unifications

  TcPluginResult -> TcPluginM TcPluginResult
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TcPluginResult -> TcPluginM TcPluginResult)
-> TcPluginResult -> TcPluginM TcPluginResult
forall a b. (a -> b) -> a -> b
$ [(EvTerm, Ct)] -> [Ct] -> TcPluginResult
TcPluginOk (PolysemyStuff 'Things -> [Ct] -> [(EvTerm, Ct)]
solveBogusError PolysemyStuff 'Things
stuff [Ct]
wanted) [Ct]
new_wanteds