Fix ambiguously looking variables in smart constructors, refactor Polysemy.Internal.TH.Common

This commit is contained in:
TheMatten 2019-07-08 21:52:29 +02:00
parent 7807c6b171
commit ec03b04e8e
4 changed files with 261 additions and 208 deletions

View File

@ -22,7 +22,7 @@ module TypeErrors where
-- ... Couldn't match expected type ...Sem r Bool... with actual type ...Bool...
-- ...
-- ... Couldn't match expected type ...Maybe a0...
-- ... with actual type ...Sem r0 a1...
-- ... with actual type ...Sem r0 s0...
-- ...
missingFmap = ()

View File

@ -1,12 +1,11 @@
{-# LANGUAGE CPP #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_HADDOCK not-home #-}
module Polysemy.Internal.TH.Common
( ConLiftInfo (..)
, getEffectMetadata
@ -17,13 +16,15 @@ module Polysemy.Internal.TH.Common
, makeEffectType
, makeUnambiguousSend
, checkExtensions
, foldArrows
, foldArrowTs
, splitArrowTs
, pattern (:->)
) where
import Control.Arrow ((>>>))
import Control.Monad
import Data.Bifunctor
import Data.Char (toLower)
import Data.Either
import Data.Generics hiding (Fixity)
import Data.List
import qualified Data.Map.Strict as M
@ -40,13 +41,115 @@ import Prelude hiding ((<>))
------------------------------------------------------------------------------
-- | Given an effect name, eg @''State@, get information about the type
-- constructor, and about each of its data constructors.
getEffectMetadata :: Name -> Q (DatatypeInfo, [ConLiftInfo])
-- Effects TH ----------------------------------------------------------------
------------------------------------------------------------------------------
------------------------------------------------------------------------------
-- | Info about constructor being lifted; use 'makeCLInfo' to create one.
data ConLiftInfo = CLInfo
{ -- | Name of effect's type constructor
cliEffName :: Name
, -- | Effect-specific type arguments
cliEffArgs :: [Type]
, -- | Result type specific to action
cliEffRes :: Type
, -- | Name of action constructor
cliConName :: Name
, -- | Name of final function
cliFunName :: Name
, -- | Fixity of function used as an operator
cliFunFixity :: Maybe Fixity
, -- | Final function arguments
cliFunArgs :: [(Name, Type)]
, -- | Constraints of final function
cliFunCxt :: Cxt
, -- | Name of type variable parameterizing 'Sem'
cliUnionName :: Name
} deriving Show
------------------------------------------------------------------------------
-- | Given an name of datatype or some of it's constructors/fields, return
-- datatype's name together with info about it's constructors.
getEffectMetadata :: Name -> Q (Name, [ConLiftInfo])
getEffectMetadata type_name = do
dt_info <- reifyDatatype type_name
cl_infos <- traverse (mkCLInfo dt_info) $ datatypeCons dt_info
pure (dt_info, cl_infos)
cl_infos <- traverse makeCLInfo $ constructorName <$> datatypeCons dt_info
pure (datatypeName dt_info, cl_infos)
------------------------------------------------------------------------------
-- | Creates name of lifting function from action name.
liftFunNameFromCon :: Name -> Name
liftFunNameFromCon n = mkName $
case nameBase n of
':' : cs -> cs
c : cs -> toLower c : cs
"" -> error "liftFunNameFromCon: empty constructor name"
------------------------------------------------------------------------------
-- | Creates info about smart constructor being created from name of the
-- original one.
makeCLInfo :: Name -> Q ConLiftInfo
makeCLInfo cliConName = do
(con_type, cliEffName) <- reify cliConName >>= \case
DataConI _ t p -> pure (t, p)
_ -> notDataCon cliConName
-- We do not support type families (polysemy-research/polysemy#157).
reify cliEffName >>= \case
FamilyI{} -> dataFamsNotSupported
_ -> pure ()
let (con_args, [con_return_type]) = splitAtEnd 1
$ splitArrowTs con_type
(ty_con_args, [monad_arg, res_arg]) <-
case splitAtEnd 2 $ tail $ splitAppTs $ con_return_type of
r@(_, [_, _]) -> pure r
_ -> missingEffArgs cliEffName
monad_name <- maybe (argNotVar cliEffName monad_arg)
pure
(tVarName monad_arg)
cliUnionName <- newName "r"
let normalize_types :: (TypeSubstitution t, Data t) => t -> t
normalize_types = replaceMArg monad_name cliUnionName
. simplifyKinds
cliEffArgs = normalize_types ty_con_args
cliEffRes = normalize_types res_arg
cliFunName = liftFunNameFromCon cliConName
cliFunFixity <- reifyFixity cliConName
fun_arg_names <- replicateM (length con_args) $ newName "x"
let cliFunArgs = zip fun_arg_names $ normalize_types con_args
-- GADTs seem to forbid constraints further in signature, so top level
-- ones should be fine.
cliFunCxt = topLevelConstraints con_type
pure CLInfo{..}
------------------------------------------------------------------------------
-- | Given a 'ConLiftInfo', get the corresponding effect type.
makeEffectType :: ConLiftInfo -> Type
makeEffectType cli = foldl' AppT (ConT $ cliEffName cli) $ cliEffArgs cli
------------------------------------------------------------------------------
-- | @'makeInterpreterType' con r a@ will produce a @'Polysemy.Sem' (Effect ':
-- r) a -> 'Polysemy.Sem' r a@ type, where @Effect@ is the effect
-- corresponding to the 'ConLiftInfo' for @con@.
makeInterpreterType :: ConLiftInfo -> Name -> Type -> Type
makeInterpreterType cli r result = sem_with_eff :-> makeSemType r result where
sem_with_eff = ConT ''Sem `AppT` r_with_eff `AppT` result
r_with_eff = PromotedConsT `AppT` makeEffectType cli `AppT` VarT r
------------------------------------------------------------------------------
@ -55,14 +158,6 @@ makeMemberConstraint :: Name -> ConLiftInfo -> Pred
makeMemberConstraint r cli = makeMemberConstraint' r $ makeEffectType cli
------------------------------------------------------------------------------
-- | Given a 'ConLiftInfo', get the corresponding effect type.
makeEffectType :: ConLiftInfo -> Type
makeEffectType cli
= foldl' AppT (ConT $ cliEffName cli)
$ cliEffArgs cli
------------------------------------------------------------------------------
-- | @'makeMemberConstraint'' r type@ will produce a @Member type r@
-- constraint.
@ -76,112 +171,45 @@ makeSemType :: Name -> Type -> Type
makeSemType r result = ConT ''Sem `AppT` VarT r `AppT` result
------------------------------------------------------------------------------
-- | @'makeInterpreterType' con r a@ will produce a @'Polysemy.Sem' (Effect ':
-- r) a -> 'Polysemy.Sem' r a@ type, where @Effect@ is the effect corresponding
-- to the 'ConLiftInfo' for @con@.
makeInterpreterType :: ConLiftInfo -> Name -> Type -> Type
makeInterpreterType cli r result =
foldArrows (makeSemType r result)
$ pure
$ ConT ''Sem
`AppT` (PromotedConsT `AppT` makeEffectType cli `AppT` VarT r)
`AppT` result
------------------------------------------------------------------------------
-- | Given a 'ConLiftInfo', this will produce an action for it. It's arguments
-- will come from any variables in scope that correspond to the 'cliArgs' of
-- the 'ConLiftInfo'.
makeUnambiguousSend :: Bool -> ConLiftInfo -> Exp
makeUnambiguousSend should_mk_sigs cli =
let fun_args_names = fmap fst $ cliArgs cli
makeUnambiguousSend should_make_sigs cli =
let fun_args_names = fmap fst $ cliFunArgs cli
action = foldl1' AppE
$ ConE (cliConName cli) : (VarE <$> fun_args_names)
eff = foldl' AppT (ConT $ cliEffName cli) $ args
-- see NOTE(makeSem_)
args = (if should_mk_sigs then id else map capturableTVars)
$ cliEffArgs cli ++ [sem, cliResType cli]
args = (if should_make_sigs then id else map capturableTVars)
$ cliEffArgs cli ++ [sem, cliEffRes cli]
sem = ConT ''Sem `AppT` VarT (cliUnionName cli)
in AppE (VarE 'send) $ SigE action eff
------------------------------------------------------------------------------
-- | Info about constructor being lifted; use 'mkCLInfo' to create one.
data ConLiftInfo = CLInfo
{ -- | Name of effect's type constructor
cliEffName :: Name
-- | Effect-specific type arguments
, cliEffArgs :: [Type]
-- | Result type specific to action
, cliResType :: Type
-- | Name of action constructor
, cliConName :: Name
-- | Name of final function
, cliFunName :: Name
-- | Fixity of function used as an operator
, cliFunFixity :: Maybe Fixity
-- | Final function arguments
, cliArgs :: [(Name, Type)]
-- | Constraints of final function
, cliFunCxt :: Cxt
-- | Name of type variable parameterizing 'Sem'
, cliUnionName :: Name
} deriving Show
-- Error messages and checks -------------------------------------------------
argNotVar :: Name -> Type -> Q a
argNotVar eff_name arg = fail $ show
$ text "Argument " <> ppr arg <> text " in effect " <> ppr eff_name
<> text " is not a type variable"
------------------------------------------------------------------------------
-- | Creates info about smart constructor being created from info about action
-- and it's parent type.
mkCLInfo :: DatatypeInfo -> ConstructorInfo -> Q ConLiftInfo
mkCLInfo dti ci = do
let cliEffName = datatypeName dti
(raw_cli_eff_args, [m_arg, raw_cli_res_arg]) <-
case splitAtEnd 2 $ datatypeInstTypes dti of
r@(_, [_, _]) -> pure r
_ -> missingEffArgs cliEffName
m_name <-
case tVarName m_arg of
Just r -> pure r
Nothing -> mArgNotVar cliEffName m_arg
cliUnionName <- newName "r"
cliFunFixity <- reifyFixity $ constructorName ci
let normalizeType = replaceMArg m_name cliUnionName
. simplifyKinds
. applySubstitution eq_pairs
-- We extract equality constraints with variables to unify them
-- manually - this makes type errors more readable. Plus we replace
-- kind of result with 'Type' if it is a type variable.
(eq_pairs, cliFunCxt) = first (M.fromList . maybeResKindToType)
$ partitionEithers
$ eqPairOrCxt <$> constructorContext ci
maybeResKindToType = maybe id (\k ps -> (k, StarT) : ps)
$ tVarName $ tvKind $ last
$ datatypeVars dti
cliEffArgs = normalizeType <$> raw_cli_eff_args
cliResType = normalizeType raw_cli_res_arg
cliConName = constructorName ci
cliFunName = liftFunNameFromCon cliConName
arg_types = normalizeType <$> constructorFields ci
arg_names <- replicateM (length arg_types) $ newName "x"
pure CLInfo{cliArgs = zip arg_names arg_types, ..}
------------------------------------------------------------------------------
-- Error messages and checks
mArgNotVar :: Name -> Type -> Q a
mArgNotVar name mArg = fail $ show
$ text "Monad argument " <> ppr mArg <> text " in effect "
<> ppr name <> text " is not a type variable"
-- | Fail the 'Q' monad whenever the given 'Extension's aren't enabled in the
-- current module.
checkExtensions :: [Extension] -> Q ()
checkExtensions exts = do
states <- zip exts <$> traverse isExtEnabled exts
maybe (pure ())
(\(ext, _) -> fail $ show
$ char '' <> text (show ext) <> char ''
<+> text "extension needs to be enabled for Polysemy's Template Haskell to work")
(find (not . snd) states)
dataFamsNotSupported :: Q a
dataFamsNotSupported = fail $ show
$ text "makesSem and makesSem_ do not support data families"
$+$ nest 4 (text "(see polysemy-research/polysemy#157)")
missingEffArgs :: Name -> Q a
missingEffArgs name = fail $ show
@ -199,80 +227,29 @@ missingEffArgs name = fail $ show
base = capturableBase name
args = PlainTV . mkName <$> ["m", "a"]
notDataCon :: Name -> Q a
notDataCon name = fail $ show
$ char '' <> ppr name <> text " is not a data constructor"
------------------------------------------------------------------------------
-- | Fail the 'Q' monad whenever the given 'Extension's aren't enabled in the
-- current module.
checkExtensions :: [Extension] -> Q ()
checkExtensions exts = do
states <- zip exts <$> traverse isExtEnabled exts
maybe (pure ())
(\(ext, _) -> fail $ show
$ char '' <> text (show ext) <> char ''
<+> text "extension needs to be enabled for Polysemy's Template Haskell to work")
(find (not . snd) states)
-- TH utilities --------------------------------------------------------------
------------------------------------------------------------------------------
------------------------------------------------------------------------------
-- | Pattern constructing function type and matching on one that may contain
-- type annotations on arrow itself.
infixr 1 :->
pattern (:->) :: Type -> Type -> Type
pattern a :-> b <- (removeTyAnns -> ArrowT) `AppT` a `AppT` b where
a :-> b = ArrowT `AppT` a `AppT` b
------------------------------------------------------------------------------
-- | Constructs capturable name from base of input name.
capturableBase :: Name -> Name
capturableBase = mkName . nameBase
------------------------------------------------------------------------------
-- | Replaces use of @m@ in type with @Sem r@.
replaceMArg :: TypeSubstitution t => Name -> Name -> t -> t
replaceMArg m r = applySubstitution $ M.singleton m $ ConT ''Sem `AppT` VarT r
------------------------------------------------------------------------------
-- Removes 'Type' and variable kind signatures from type.
simplifyKinds :: Type -> Type
simplifyKinds = everywhere $ mkT $ \case
SigT t StarT -> t
SigT t VarT{} -> t
ForallT bs cs t -> ForallT (goBndr <$> bs) (simplifyKinds <$> cs) t
where
goBndr (KindedTV n StarT ) = PlainTV n
goBndr (KindedTV n VarT{}) = PlainTV n
goBndr b = b
t -> t
------------------------------------------------------------------------------
-- | Converts equality constraint with type variable to name and type pair if
-- possible or leaves constraint as is.
eqPairOrCxt :: Pred -> Either (Name, Type) Pred
eqPairOrCxt p = case asEqualPred p of
Just (VarT n, b) -> Left (n, b)
Just (a, VarT n) -> Left (n, a)
_ -> Right p
------------------------------------------------------------------------------
-- | Creates name of lifting function from action name.
liftFunNameFromCon :: Name -> Name
liftFunNameFromCon n = mkName $
case nameBase n of
':' : cs -> cs
c : cs -> toLower c : cs
"" -> error "liftFunNameFromCon: empty constructor name"
------------------------------------------------------------------------------
-- | Folds a list of 'Type's into a right-associative arrow 'Type'.
foldArrows :: Type -> [Type] -> Type
foldArrows = foldr (AppT . AppT ArrowT)
------------------------------------------------------------------------------
-- | Extracts name from type variable (possibly nested in signature and/or
-- some context), returns 'Nothing' otherwise.
tVarName :: Type -> Maybe Name
tVarName = \case
ForallT _ _ t -> tVarName t
SigT t _ -> tVarName t
VarT n -> Just n
ParensT t -> tVarName t
_ -> Nothing
------------------------------------------------------------------------------
-- | 'splitAt' counting from the end.
splitAtEnd :: Int -> [a] -> ([a], [a])
splitAtEnd n = swap . join bimap reverse . splitAt n . reverse
------------------------------------------------------------------------------
-- | Converts names of all type variables in type to capturable ones based on
@ -286,3 +263,77 @@ capturableTVars = everywhere $ mkT $ \case
goBndr (KindedTV n k) = KindedTV (capturableBase n) $ capturableTVars k
t -> t
------------------------------------------------------------------------------
-- | Folds a list of 'Type's into a right-associative arrow 'Type'.
foldArrowTs :: Type -> [Type] -> Type
foldArrowTs = foldr (:->)
------------------------------------------------------------------------------
-- | Replaces use of @m@ in type with @Sem r@.
replaceMArg :: TypeSubstitution t => Name -> Name -> t -> t
replaceMArg m r = applySubstitution $ M.singleton m $ ConT ''Sem `AppT` VarT r
------------------------------------------------------------------------------
-- Removes 'Type' and variable kind signatures from type.
simplifyKinds :: Data t => t -> t
simplifyKinds = everywhere $ mkT $ \case
SigT t StarT -> t
SigT t VarT{} -> t
ForallT bs cs t -> ForallT (goBndr <$> bs) (simplifyKinds <$> cs) t
where
goBndr (KindedTV n StarT ) = PlainTV n
goBndr (KindedTV n VarT{}) = PlainTV n
goBndr b = b
t -> t
------------------------------------------------------------------------------
splitAppTs :: Type -> [Type]
splitAppTs = removeTyAnns >>> \case
t `AppT` arg -> splitAppTs t ++ [arg]
t -> [t]
------------------------------------------------------------------------------
splitArrowTs :: Type -> [Type]
splitArrowTs = removeTyAnns >>> \case
t :-> ts -> t : splitArrowTs ts
t -> [t]
------------------------------------------------------------------------------
-- | Extracts name from type variable (possibly nested in signature and/or
-- some context), returns 'Nothing' otherwise.
tVarName :: Type -> Maybe Name
tVarName = removeTyAnns >>> \case
VarT n -> Just n
_ -> Nothing
------------------------------------------------------------------------------
topLevelConstraints :: Type -> Cxt
topLevelConstraints = \case
ForallT _ cs _ -> cs
_ -> []
------------------------------------------------------------------------------
removeTyAnns :: Type -> Type
removeTyAnns = \case
ForallT _ _ t -> removeTyAnns t
SigT t _ -> removeTyAnns t
ParensT t -> removeTyAnns t
t -> t
------------------------------------------------------------------------------
-- Miscellaneous -------------------------------------------------------------
------------------------------------------------------------------------------
------------------------------------------------------------------------------
-- | 'splitAt' counting from the end.
splitAtEnd :: Int -> [a] -> ([a], [a])
splitAtEnd n = swap . join bimap reverse . splitAt n . reverse

View File

@ -1,9 +1,6 @@
{-# OPTIONS_HADDOCK not-home #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TupleSections #-}
{-# OPTIONS_HADDOCK not-home #-}
-- | This module provides Template Haskell functions for automatically generating
-- effect operation functions (that is, functions that use 'send') from a given
@ -38,6 +35,7 @@ import Language.Haskell.TH.Datatype
import Polysemy.Internal.CustomErrors (DefiningModule)
import Polysemy.Internal.TH.Common
-- TODO: write tests for what should (not) compile
------------------------------------------------------------------------------
@ -79,7 +77,7 @@ makeSem = genFreer True
-- * signatures have to specify argument of 'Sem' representing union of
-- effects as @r@ (e.g. @'Sem' r ()@)
-- * all arguments in effect's type constructor have to follow naming scheme
-- from effect's declaration:
-- from data constructor's declaration:
--
-- @
-- data Foo e m a where
@ -87,11 +85,11 @@ makeSem = genFreer True
-- FooC2 :: Foo (Maybe x) m ()
-- @
--
-- should have @e@ in type signature of @fooC1@:
-- should have @x@ in type signature of @fooC1@:
--
-- @fooC1 :: forall e r. Member (Foo e) r => Sem r ()@
-- @fooC1 :: forall x r. Member (Foo x) r => Sem r ()@
--
-- but @x@ in signature of @fooC2@:
-- and @Maybe x@ in signature of @fooC2@:
--
-- @fooC2 :: forall x r. Member (Foo (Maybe x)) r => Sem r ()@
--
@ -101,16 +99,19 @@ makeSem = genFreer True
-- These restrictions may be removed in the future, depending on changes to
-- the compiler.
--
-- Change in (TODO(Sandy): version): in case of GADTs, signatures now only use
-- names from data constructor's type and not from type constructor
-- declaration.
--
-- @since 0.1.2.0
makeSem_ :: Name -> Q [Dec]
makeSem_ = genFreer False
-- NOTE(makeSem_):
-- This function uses an ugly hack to work --- it enables change of names in
-- annotation of applied data constructor to capturable ones, based of names
-- in effect's definition. This allows user to provide them to us from their
-- signature through 'forall' with 'ScopedTypeVariables' enabled, so that we
-- can compile liftings of constructors with ambiguous type arguments (see
-- issue #48).
-- This function uses an ugly hack to work --- it changes names in data
-- constructor's type to capturable ones. This allows user to provide them to
-- us from their signature through 'forall' with 'ScopedTypeVariables'
-- enabled, so that we can compile liftings of constructors with ambiguous
-- type arguments (see issue #48).
--
-- Please, change this as soon as GHC provides some way of inspecting
-- signatures, replacing code or generating haddock documentation in TH.
@ -122,12 +123,12 @@ makeSem_ = genFreer False
genFreer :: Bool -> Name -> Q [Dec]
genFreer should_mk_sigs type_name = do
checkExtensions [ScopedTypeVariables, FlexibleContexts]
(dt_info, cl_infos) <- getEffectMetadata type_name
(dt_name, cl_infos) <- getEffectMetadata type_name
tyfams_on <- isExtEnabled TypeFamilies
def_mod_fi <- sequence [ tySynInstDCompat
''DefiningModule
Nothing
[pure . ConT $ datatypeName dt_info]
[pure $ ConT dt_name]
(LitT . StrTyLit . loc_module <$> location)
| tyfams_on
]
@ -146,13 +147,13 @@ genSig cli
= maybe [] (pure . flip InfixD (cliFunName cli)) (cliFunFixity cli)
++ [ SigD (cliFunName cli) $ quantifyType
$ ForallT [] (member_cxt : cliFunCxt cli)
$ foldArrows sem
$ foldArrowTs sem
$ fmap snd
$ cliArgs cli
$ cliFunArgs cli
]
where
member_cxt = makeMemberConstraint (cliUnionName cli) cli
sem = makeSemType (cliUnionName cli) (cliResType cli)
sem = makeSemType (cliUnionName cli) (cliEffRes cli)
------------------------------------------------------------------------------
@ -160,7 +161,7 @@ genSig cli
-- @x a b c = send (X a b c :: E m a)@.
genDec :: Bool -> ConLiftInfo -> Q [Dec]
genDec should_mk_sigs cli = do
let fun_args_names = fmap fst $ cliArgs cli
let fun_args_names = fmap fst $ cliFunArgs cli
pure
[ PragmaD $ InlineP (cliFunName cli) Inlinable ConLike AllPhases

View File

@ -36,7 +36,7 @@ data GADTSyntax m a where
makeSem ''GADTSyntax
data ADTSyntax1 m a = (a ~ Int) => ADTSyntax1C String
data ADTSyntax1 m a = a ~ Int => ADTSyntax1C String
makeSem ''ADTSyntax1
@ -68,24 +68,25 @@ newtype Newtype2 m a where
makeSem ''Newtype2
-- Data families -------------------------------------------------------------
-- NOTE: Not supported currently, but may be reconsidered in the future.
data Instance = ADTI | GADTI | NTI
-- data Instance = ADTI | GADTI | NTI
data family Family (s :: Instance) (m :: Type -> Type) a
-- data family Family (s :: Instance) (m :: Type -> Type) a
data instance Family 'ADTI m a = ADTIC1 Int | ADTIC2 String
-- data instance Family 'ADTI m a = ADTIC1 Int | ADTIC2 String
makeSem 'ADTIC1
-- makeSem 'ADTIC1
data instance Family 'GADTI m a where
GADTIC1 :: Int -> Family 'GADTI m Int
GADTIC2 :: String -> Family 'GADTI m String
-- data instance Family 'GADTI m a where
-- GADTIC1 :: Int -> Family 'GADTI m Int
-- GADTIC2 :: String -> Family 'GADTI m String
makeSem 'GADTIC1
-- makeSem 'GADTIC1
newtype instance Family 'NTI m a = NTIC Int
-- newtype instance Family 'NTI m a = NTIC Int
makeSem 'NTIC
-- makeSem 'NTIC
-- Phantom types -------------------------------------------------------------