{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -Wall #-}
module Plugin.MagicTyFam
( magicTyFamPlugin
, withStuckSemantics
, isTyFamFree
, solveWanteds
, loadTyCon
, WhenStuck
, Plugin
, TyCon
, Type
) where
import Control.Monad (guard)
import Data.Generics (everything, mkQ)
import Data.Traversable (for)
import GHC.TcPluginM.Extra (lookupModule, lookupName, evByFiat)
import GhcPlugins
import TcEvidence (EvTerm (..))
import TcPluginM (TcPluginM, tcLookupTyCon, newGiven)
import TcRnTypes
import TcType (isTyFamFree)
loadTyCon
:: String
-> String
-> String
-> TcPluginM TyCon
loadTyCon p m i = do
md <- lookupModule (mkModuleName m) $ fsLit p
nm <- lookupName md $ mkTcOcc i
tcLookupTyCon nm
magicTyFamPlugin
:: String
-> String
-> String
-> ([Type] -> Maybe Type)
-> Plugin
magicTyFamPlugin p m i f = defaultPlugin
{ tcPlugin = const $ Just $ TcPlugin
{ tcPluginInit = loadTyCon p m i
, tcPluginSolve = \cmp_type _ _ w ->
TcPluginOk [] <$> solveWanteds f cmp_type w
, tcPluginStop = const $ pure ()
}
, pluginRecompile = const $ pure NoForceRecompile
}
withStuckSemantics :: ([Type] -> Maybe Type) -> [Type] -> Maybe Type
withStuckSemantics f ts = do
guard $ all isTyFamFree ts
f ts
solveWanteds :: ([Type] -> Maybe Type) -> TyCon -> [Ct] -> TcPluginM [Ct]
solveWanteds _ _ [] = pure []
solveWanteds f cmp_type wanted = do
let rel = fmap (findRelevant f cmp_type . ctLoc <*> ctev_pred . cc_ev) wanted
gs <- for (concat rel) $ \(MagicTyFamResult loc t res) -> do
let EvExpr ev = evByFiat "magic-tyfams" t res
newGiven loc (mkPrimEqPred t res) ev
pure $ fmap CNonCanonical gs
findRelevant :: ([Type] -> Maybe Type) -> TyCon -> CtLoc -> Type -> [MagicTyFamResult]
findRelevant f cmp_type loc = everything (++) $ mkQ [] findCmpType
where
findCmpType t =
case splitTyConApp_maybe t of
Just (tc, ts) | tc == cmp_type ->
maybe [] (pure . MagicTyFamResult loc t) $ f ts
_ -> []
data MagicTyFamResult = MagicTyFamResult
{ _mtfrLoc :: CtLoc
, _mtfrOriginal :: Type
, _mtfrSolved :: Type
}
type family WhenStuck (expr :: k) (b :: k) :: k where
WhenStuck (_ AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
AnythingOfAnyKind) b = b
WhenStuck a b = a
data AnythingOfAnyKind