Revert "Let plugin solve stuck type rows + bug fixes in interpreter mode (#245)" (#249)

This reverts commit 7a009f70b6.
This commit is contained in:
Sandy Maguire 2019-10-09 14:35:07 +02:00 committed by GitHub
parent 7a009f70b6
commit a86aec37fb
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
7 changed files with 65 additions and 333 deletions

View File

@ -4,7 +4,7 @@ cabal-version: 1.12
--
-- see: https://github.com/sol/hpack
--
-- hash: 6aabb881334585f56358446f23bcdff48fa22af05afc52c83a102db79c9ccd06
-- hash: 01634ce3c7ac101e60c1a02f8ccad7ec499c02a04b66e5d9dd5993f314318097
name: polysemy-plugin
version: 0.2.3.0
@ -57,11 +57,9 @@ test-suite polysemy-plugin-test
BadSpec
DoctestSpec
ExampleSpec
HistorySpec
LegitimateTypeErrorSpec
MultipleVarsSpec
PluginSpec
SpecificitySpec
TypeErrors
VDQSpec
Paths_polysemy_plugin

View File

@ -1,16 +1,6 @@
{-# LANGUAGE CPP #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE ViewPatterns #-}
#if MIN_VERSION_ghc(8,5,0)
#else
#define EvExpr
#define Coercion EvCoercion
-- #if __GLASGOW_HASKELL__ < 711
-- $ TcCoercion
-- #endif
#endif
------------------------------------------------------------------------------
-- The MIT License (MIT)
--
@ -43,31 +33,29 @@
module Polysemy.Plugin.Fundep (fundepPlugin) where
import Control.Applicative (empty)
import Control.Arrow ((&&&))
import Control.Monad
import CoreSyn
import Data.Bifunctor
import Data.Coerce
import Data.List (sortBy, find)
import Data.IORef
import qualified Data.Map as M
import Data.Maybe
import Data.Ord (Down (..), comparing)
import GHC.TcPluginM.Extra (evByFiat)
import GhcPlugins hiding (empty)
import Outputable hiding (empty)
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, newGiven)
import TcPluginM (TcPluginM, tcPluginIO)
import TcRnTypes
import TcSMonad hiding (tcLookupClass)
import Type
fundepPlugin :: TcPlugin
fundepPlugin = TcPlugin
{ tcPluginInit = polysemyStuff
{ tcPluginInit =
(,) <$> tcPluginIO (newIORef S.empty)
<*> polysemyStuff
, tcPluginSolve = solveFundep
, tcPluginStop = const $ pure ()
}
@ -114,15 +102,6 @@ findMatchingEffectIfSingular (FindConstraint _ eff_name wanted r) ts =
pure eff'
oneMostSpecific :: [Type] -> Maybe Type
oneMostSpecific tys =
let sorted = sortBy (comparing $ Down . fst) $ fmap (specificityMetric &&& id) tys
in case pprTrace "sorted" (ppr sorted) sorted of
((p1, t1) : (p2, _) : _) | p1 /= p2 -> Just t1
[(_, t1)] -> Just t1
_ -> Nothing
------------------------------------------------------------------------------
-- | Given an effect, compute its effect name.
getEffName :: Type -> Type
@ -132,16 +111,17 @@ getEffName t = fst $ splitAppTys t
------------------------------------------------------------------------------
-- | Generate a wanted unification for the effect described by the
-- 'FindConstraint' and the given effect.
mkGivenForce
mkWantedForce
:: FindConstraint
-> Type
-> TcPluginM Unification
mkGivenForce fc given = do
ev <- newGiven (fcLoc fc) (mkPrimEqPred wanted given)
. Coercion
$ mkTcNomReflCo given
pure . Unification (OrdType wanted) (OrdType given)
$ CNonCanonical ev
-> TcPluginM (Unification, Ct)
mkWantedForce fc given = do
(ev, _) <- unsafeTcPluginTcM
. runTcSDeriveds
$ newWantedEq (fcLoc fc) Nominal wanted given
pure ( Unification (OrdType wanted) (OrdType given)
, CNonCanonical ev
)
where
wanted = fcEffect fc
@ -149,14 +129,14 @@ mkGivenForce fc given = do
-- | Generate a wanted unification for the effect described by the
-- 'FindConstraint' and the given effect --- if they can be unified in this
-- context.
mkGiven
mkWanted
:: FindConstraint
-> SolveContext
-> Type -- ^ The given effect.
-> TcPluginM (Maybe Unification)
mkGiven fc solve_ctx given =
-> TcPluginM (Maybe (Unification, Ct))
mkWanted fc solve_ctx given =
whenA (not (mustUnify solve_ctx) || canUnifyRecursive solve_ctx wanted given) $
mkGivenForce fc given
mkWantedForce fc given
where
wanted = fcEffect fc
@ -219,13 +199,15 @@ exactlyOneWantedForR wanteds
solveFundep
:: PolysemyStuff 'Things
:: ( IORef (S.Set Unification)
, PolysemyStuff 'Things
)
-> [Ct]
-> [Ct]
-> [Ct]
-> TcPluginM TcPluginResult
solveFundep _ _ _ [] = pure $ TcPluginOk [] []
solveFundep stuff given _ wanted = do
solveFundep (ref, stuff) given _ wanted = do
let wanted_finds = getFindConstraints stuff wanted
given_finds = getFindConstraints stuff given
@ -235,106 +217,24 @@ solveFundep stuff given _ wanted = do
-- 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 eff' -> Just <$> mkGivenForce fc eff'
Just eff' -> Just <$> mkWantedForce fc 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!
Nothing ->
case splitAppTys r of
(_, [_, eff', _]) -> do
mkGiven fc
(_, [_, eff', _]) ->
mkWanted fc
(InterpreterUse $ exactlyOneWantedForR wanted_finds r)
eff'
_ -> pure Nothing
let unifications = getGoodUnifications $ catMaybes eqs
new_givens = fmap _unifyCt unifications
-- We only want to emit a unification wanted once, otherwise a type error can
-- force the type checker to loop forever.
already_emitted <- tcPluginIO $ readIORef ref
let (unifications, new_wanteds) = unzipNewWanteds already_emitted $ catMaybes eqs
tcPluginIO $ modifyIORef ref $ S.union $ S.fromList unifications
solved_founds <- getFounds stuff wanted
solved_indexofs <- getIndexOfFounds stuff wanted
pure $ TcPluginOk (solveBogusError stuff wanted) $
mconcat
[ new_givens
, solved_founds
, solved_indexofs
]
------------------------------------------------------------------------------
-- | Unroll a row into all the types that are consed together in it.
unrollR :: Type -> [Type]
unrollR r =
case splitAppTys r of
(_, [_, eff', r']) -> eff' : unrollR r'
_ -> [r]
------------------------------------------------------------------------------
-- | Solves stuck type families of the form @IndexOf row (Found row e) ~ e@.
-- This can happen when we're in interpreter mode, searching for effects in the
-- row that have type variables that should /stay/ type variables.
getIndexOfFounds :: PolysemyStuff 'Things -> [Ct] -> TcPluginM [Ct]
getIndexOfFounds stuff cts = sequenceA $ do
ct@(CNonCanonical ev) <- cts
let ctpred = ctev_pred ev
Just (_, t1, e) <- pure $ getEqPredTys_maybe ctpred
Just (indexOfTc, [_, r, n]) <- pure $ splitTyConApp_maybe t1
guard $ indexOfTc == indexOfTyCon stuff
Just (foundTc, [_, r', e']) <- pure $ splitTyConApp_maybe n
guard $ foundTc == foundTyCon stuff
guard $ eqType r r'
guard $ eqType e e'
let EvExpr evidence = evByFiat "polysemy-plugin" t1 e
pure $ CNonCanonical <$> newGiven (ctLoc ct) (mkPrimEqPred t1 e) evidence
------------------------------------------------------------------------------
-- | Solves stuck type families of the form @Found row e ~ nat@, by determining
-- whether or not @e@ is actually at @nat@ in @row@. GHC should actually do
-- this on its own, but doesn't due to
-- https://gitlab.haskell.org/ghc/ghc/issues/17311
getFounds :: PolysemyStuff 'Things -> [Ct] -> TcPluginM [Ct]
getFounds stuff cts = sequenceA $ do
ct@(CNonCanonical ev) <- cts
let evpred = ctev_pred ev
Just (_, t1, nat) <- pure $ getEqPredTys_maybe evpred
Just (foundTc, [_, r, e]) <- pure $ splitTyConApp_maybe t1
guard $ foundTc == foundTyCon stuff
let EvExpr evidence = evByFiat "polysemy-plugin" t1 nat
let unrolled = unrollR r
proof = CNonCanonical <$> newGiven (ctLoc ct) (mkPrimEqPred t1 nat) evidence
case fmap fst $ find (eqType e . snd) $ zip [0..] unrolled of
Just index -> do
guard $ mkNat stuff index `eqType` nat
pure proof
Nothing -> do
let n = stripS stuff nat
case drop n unrolled of
[t] | isTyVarTy t -> pure proof
_ -> empty
------------------------------------------------------------------------------
-- | Turn an 'Int' into a 'Polysemy.Internal.Union.Nat'.
mkNat :: PolysemyStuff 'Things -> Int -> Type
mkNat stuff = go
where
go 0 = mkTyConTy $ promotedZDataCon stuff
go n = mkTyConApp (promotedSDataCon stuff) [go $ n - 1]
------------------------------------------------------------------------------
-- | Counts the number of 'Polysemy.Internal.Union.S' constructors in a type.
stripS :: PolysemyStuff 'Things -> Type -> Int
stripS stuff = go
where
go (splitTyConApp_maybe -> Just (tc, [a]))
| tc == promotedSDataCon stuff
= 1 + go a
go _ = 0
pure $ TcPluginOk (solveBogusError stuff wanted) new_wanteds

View File

@ -1,5 +1,3 @@
{-# LANGUAGE AllowAmbiguousTypes #-}
module Polysemy.Plugin.Fundep.Stuff
( PolysemyStuff (..)
, LookupState (..)
@ -8,11 +6,10 @@ module Polysemy.Plugin.Fundep.Stuff
import Data.Kind (Type)
import FastString (fsLit)
import GHC (Name, Class, TyCon, DataCon, mkModuleName)
import GHC (Name, Class, TyCon, mkModuleName)
import GHC.TcPluginM.Extra (lookupModule, lookupName)
import OccName (OccName, mkTcOcc, mkDataOcc)
import TcPluginM (TcPluginM, tcLookupClass, tcLookupTyCon, tcLookupDataCon)
import DataCon (promoteDataCon)
import OccName (mkTcOcc)
import TcPluginM (TcPluginM, tcLookupClass, tcLookupTyCon)
@ -21,13 +18,10 @@ import DataCon (promoteDataCon)
-- When @l ~ 'Locations@, each of these is just a pair of strings. When @l
-- ~ 'Things@, it's actually references to the stuff.
data PolysemyStuff (l :: LookupState) = PolysemyStuff
{ findClass :: ThingOf l Class
, foundTyCon :: ThingOf l TyCon
, semTyCon :: ThingOf l TyCon
, ifStuckTyCon :: ThingOf l TyCon
, indexOfTyCon :: ThingOf l TyCon
, promotedSDataCon :: ThingOf l TyCon
, promotedZDataCon :: ThingOf l TyCon
{ findClass :: ThingOf l Class
, semTyCon :: ThingOf l TyCon
, ifStuckTyCon :: ThingOf l TyCon
, indexOfTyCon :: ThingOf l TyCon
}
@ -35,13 +29,10 @@ data PolysemyStuff (l :: LookupState) = PolysemyStuff
-- | All of the things we need to lookup.
polysemyStuffLocations :: PolysemyStuff 'Locations
polysemyStuffLocations = PolysemyStuff
{ findClass = ("Polysemy.Internal.Union", "Find")
, foundTyCon = ("Polysemy.Internal.Union", "Found")
, semTyCon = ("Polysemy.Internal", "Sem")
, ifStuckTyCon = ("Polysemy.Internal.CustomErrors.Redefined", "IfStuck")
, indexOfTyCon = ("Polysemy.Internal.Union", "IndexOf")
, promotedSDataCon = ("Polysemy.Internal.Union", "S")
, promotedZDataCon = ("Polysemy.Internal.Union", "Z")
{ findClass = ("Polysemy.Internal.Union", "Find")
, semTyCon = ("Polysemy.Internal", "Sem")
, ifStuckTyCon = ("Polysemy.Internal.CustomErrors.Redefined", "IfStuck")
, indexOfTyCon = ("Polysemy.Internal.Union", "IndexOf")
}
@ -49,14 +40,11 @@ polysemyStuffLocations = PolysemyStuff
-- | Lookup all of the 'PolysemyStuff'.
polysemyStuff :: TcPluginM (PolysemyStuff 'Things)
polysemyStuff =
let PolysemyStuff a b c d e f g = polysemyStuffLocations
let PolysemyStuff a b c d = polysemyStuffLocations
in PolysemyStuff <$> doLookup a
<*> doLookup b
<*> doLookup c
<*> doLookup d
<*> doLookup e
<*> (fmap promoteDataCon $ doLookup f)
<*> (fmap promoteDataCon $ doLookup g)
------------------------------------------------------------------------------
@ -77,26 +65,19 @@ type family ThingOf (l :: LookupState) (a :: Type) :: Type where
-- | Things that can be found in a 'TcPluginM' environment.
class CanLookup a where
lookupStrategy :: Name -> TcPluginM a
mkLookupOcc :: String -> OccName
instance CanLookup Class where
lookupStrategy = tcLookupClass
mkLookupOcc = mkTcOcc
instance CanLookup TyCon where
lookupStrategy = tcLookupTyCon
mkLookupOcc = mkTcOcc
instance CanLookup DataCon where
lookupStrategy = tcLookupDataCon
mkLookupOcc = mkDataOcc
------------------------------------------------------------------------------
-- | Transform a @'ThingOf' 'Locations@ into a @'ThingOf' 'Things@.
doLookup :: forall a. CanLookup a => ThingOf 'Locations a -> TcPluginM (ThingOf 'Things a)
doLookup :: CanLookup a => ThingOf 'Locations a -> TcPluginM (ThingOf 'Things a)
doLookup (mdname, name) = do
md <- lookupModule (mkModuleName mdname) $ fsLit "polysemy"
nm <- lookupName md $ mkLookupOcc @a name
nm <- lookupName md $ mkTcOcc name
lookupStrategy nm

View File

@ -1,14 +1,8 @@
module Polysemy.Plugin.Fundep.Unification where
import Control.Arrow ((&&&))
import Data.Bool
import Data.Function (on)
import Data.Generics
import Data.List
import Data.Ord
import qualified Data.Set as S
import DataCon (DataCon)
import Outputable hiding ((<>))
import TcRnTypes
import Type
@ -111,37 +105,8 @@ canUnify poly_given_ok wt gt =
data Unification = Unification
{ _unifyLHS :: OrdType
, _unifyRHS :: OrdType
, _unifyCt :: Ct
}
instance Eq Unification where
Unification a b _ == Unification a' b' _ = a == a' && b == b'
instance Ord Unification where
Unification a b _ `compare` Unification a' b' _ = compare a a' <> compare b b'
instance Outputable Unification where
ppr (Unification (OrdType a) (OrdType b) _) = ppr a <+> text " --> " <+> ppr b
getGoodUnifications :: [Unification] -> [Unification]
getGoodUnifications = fmap mostSpecificUnification . groupUnifications
groupUnifications :: [Unification] -> [[Unification]]
groupUnifications = fmap (fmap snd)
. groupBy ((==) `on` fst)
. sortBy (comparing fst)
. fmap (_unifyRHS &&& id)
specificityMetric :: Type -> Int
specificityMetric = everything (+) $ mkQ 0 $ \case
(dc :: Type) -> 1
mostSpecificUnification :: [Unification] -> Unification
mostSpecificUnification
= head . sortBy (comparing $ Down . specificityMetric . getOrdType . _unifyLHS)
deriving (Eq, Ord)
------------------------------------------------------------------------------
@ -158,3 +123,14 @@ instance Eq OrdType where
instance Ord OrdType where
compare = nonDetCmpType `on` getOrdType
------------------------------------------------------------------------------
-- | Filter out the unifications we've already emitted, and then give back the
-- things we should put into the @S.Set Unification@, and the new constraints
-- we should emit.
unzipNewWanteds
:: S.Set Unification
-> [(Unification, Ct)]
-> ([Unification], [Ct])
unzipNewWanteds old = unzip . filter (not . flip S.member old . fst)

View File

@ -1,5 +1,4 @@
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TemplateHaskell #-}
{-# OPTIONS_GHC -fdefer-type-errors -fno-warn-deferred-type-errors #-}
@ -15,10 +14,6 @@ data KVStore k v m a where
makeSem ''KVStore
runKVStore :: [(k, v)] -> InterpreterFor (KVStore k v) r
runKVStore = interpret $ \case
GetKV _ -> pure Nothing
positivePos :: Member (KVStore k v) r => Sem r (Maybe v)
positivePos = do
getKV "hello"
@ -35,12 +30,9 @@ spec :: Spec
spec = do
describe "incorrectly polymorphic constraint" $ do
it "should not typecheck in positive position" $ do
shouldNotTypecheck (run . runKVStore [("hello", True)]
$ positivePos @String @Bool @'[KVStore String Bool])
shouldNotTypecheck positivePos
it "should not typecheck in negative position" $ do
shouldNotTypecheck (run . runKVStore [("hello", True)]
$ negativePos @Bool @'[KVStore String Bool])
shouldNotTypecheck negativePos
it "should not typecheck badly polymorphic State" $ do
shouldNotTypecheck (run . runState ()
$ badState @() @'[State ()])
shouldNotTypecheck badState

View File

@ -1,84 +0,0 @@
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -fplugin=Polysemy.Plugin -fconstraint-solver-iterations=10 #-}
module HistorySpec where
import Polysemy
import Polysemy.State
import Test.Hspec
data History s m a where
Undo :: History s m ()
Redo :: History s m ()
PutAndForget :: s -> History s m ()
makeSem ''History
spec :: Spec
spec = describe "HistorySpec" $ it "should compile" $ do
let z = run . runState (0 :: Int) . runHistory $ do
modify (+ 5)
undo
x <- get
redo
y <- get
undo
put 1
redo
pure (x, y)
z `shouldBe` (1 :: Int, (0 :: Int, 5 :: Int))
data Zipper a = Zipper [a] a [a]
focusZ :: Zipper a -> a
focusZ (Zipper _ a _) = a
modifyZ :: (a -> a) -> Zipper a -> Zipper a
modifyZ f (Zipper past a _) = Zipper (a : past) (f a) []
goBack :: Zipper a -> Zipper a
goBack z@(Zipper [] _ _) = z
goBack (Zipper (p : ps) a fs) = Zipper ps p (a : fs)
goForward :: Zipper a -> Zipper a
goForward z@(Zipper _ _ []) = z
goForward (Zipper ps a (f : fs)) = Zipper (a : ps) f fs
runHistory
:: forall s r a
. Member (State s) r
=> Sem (History s ': r) a
-> Sem r a
runHistory m = do
s <- get
evalState (Zipper [] s [])
. interpret (\case
Undo -> do
s' <- modify goBack >> gets focusZ
put s'
Redo -> do
s' <- modify goForward >> gets focusZ
put s'
PutAndForget s' ->
put s')
. intercept @(State s) (\case
Get -> get
Put s' -> do
modify $ modifyZ $ const s'
put s')
. raiseUnder @(State (Zipper s))
$ m

View File

@ -1,31 +0,0 @@
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -fplugin=Polysemy.Plugin #-}
module SpecificitySpec where
import Polysemy
import Polysemy.State
import Polysemy.Internal
import Polysemy.Internal.Union
import Test.Hspec
import Data.Functor.Identity
spec :: Spec
spec = describe "HistorySpec" $ it "should compile" $ True `shouldBe` True
foo :: Members [State s, State (Identity s)] r => Sem r ()
foo = do
s <- get
put $ Identity s