diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,12 @@ +# optics-th-0.3 (2020-04-15) +* `optics-core-0.3` compatible release +* GHC-8.10 support +* Improvements to TH-generated optics: + - `LabelOptic` instances make optic kind a type equality for better type inference + - `LabelOptic` instances for field optics work properly in the presence of type families + - Fixed calculation of phantom types in `LabelOptic` prism instances + - Better support for generating optics in the presence of kind polymorphism + # optics-th-0.2 (2019-10-18) * Add `noPrefixFieldLabels` and `noPrefixNamer` to `Optics.TH` diff --git a/optics-th.cabal b/optics-th.cabal --- a/optics-th.cabal +++ b/optics-th.cabal @@ -1,12 +1,12 @@ name: optics-th -version: 0.2 +version: 0.3 license: BSD3 license-file: LICENSE build-type: Simple maintainer: optics@well-typed.com author: Andrzej Rybczak cabal-version: 1.24 -tested-with: ghc ==8.0.2 || ==8.2.2 || ==8.4.4 || ==8.6.5 || ==8.8.1, GHCJS ==8.4 +tested-with: ghc ==8.0.2 || ==8.2.2 || ==8.4.4 || ==8.6.5 || ==8.8.3 || ==8.10.1, GHCJS ==8.4 synopsis: Optics construction using TemplateHaskell category: Data, Optics, Lenses description: @@ -32,8 +32,8 @@ build-depends: base >= 4.9 && <5 , containers >= 0.5.7.1 && <0.7 , mtl >= 2.2.2 && <2.3 - , optics-core >= 0.2 && <0.3 - , template-haskell >= 2.11 && <2.16 + , optics-core >= 0.3 && <0.4 + , template-haskell >= 2.11 && <2.17 , th-abstraction >= 0.2.1 && <0.4 , transformers >= 0.5 && <0.6 @@ -54,6 +54,7 @@ build-depends: base , optics-core , optics-th + , tagged type: exitcode-stdio-1.0 main-is: Optics/TH/Tests.hs diff --git a/src/Language/Haskell/TH/Optics/Internal.hs b/src/Language/Haskell/TH/Optics/Internal.hs --- a/src/Language/Haskell/TH/Optics/Internal.hs +++ b/src/Language/Haskell/TH/Optics/Internal.hs @@ -1,10 +1,13 @@ -{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE LambdaCase #-} module Language.Haskell.TH.Optics.Internal ( -- * Traversals HasTypeVars(..) , typeVars -- :: HasTypeVars t => Traversal' t Name + , typeVarsKinded , substTypeVars -- :: HasTypeVars t => Map Name Name -> t -> t + , SubstType(..) -- * Prisms , _FamilyI @@ -15,6 +18,7 @@ import Data.Map as Map hiding (map, toList) import Data.Maybe (fromMaybe) +import Data.Foldable (traverse_) import Data.Set as Set hiding (map, toList) import Language.Haskell.TH @@ -55,7 +59,8 @@ VarT n -> VarT <$> traverseOf (typeVarsEx s) f n AppT l r -> AppT <$> traverseOf (typeVarsEx s) f l <*> traverseOf (typeVarsEx s) f r - SigT t k -> (`SigT` k) <$> traverseOf (typeVarsEx s) f t + SigT t k -> SigT <$> traverseOf (typeVarsEx s) f t + <*> traverseOf (typeVarsEx s) f k ForallT bs ctx ty -> let s' = s `Set.union` setOf typeVars bs in ForallT bs <$> traverseOf (typeVarsEx s') f ctx <*> traverseOf (typeVarsEx s') f ty @@ -66,6 +71,11 @@ <*> pure n <*> traverseOf (typeVarsEx s) f t2 ParensT t -> ParensT <$> traverseOf (typeVarsEx s) f t +#if MIN_VERSION_template_haskell(2,15,0) + AppKindT t k -> AppKindT <$> traverseOf (typeVarsEx s) f t + <*> traverseOf (typeVarsEx s) f k + ImplicitParamT n t -> ImplicitParamT n <$> traverseOf (typeVarsEx s) f t +#endif t -> pure t instance HasTypeVars t => HasTypeVars [t] where @@ -76,6 +86,27 @@ typeVars :: HasTypeVars t => Traversal' t Name typeVars = typeVarsEx mempty +-- | Traverse /free/ type variables paired with their kinds if applicable. +typeVarsKinded :: Fold Type Type +typeVarsKinded = foldVL $ go mempty + where + go s f = \case + var@(VarT n) -> if n `Set.member` s then pure () else f var + var@(SigT (VarT n) _) -> if n `Set.member` s then pure () else f var + + AppT l r -> go s f l *> go s f r + SigT t k -> go s f t *> go s f k + ForallT bs ctx ty -> let s' = s `Set.union` setOf typeVars bs + in traverse_ (go s' f) ctx *> go s' f ty + InfixT t1 _ t2 -> go s f t1 *> go s f t2 + UInfixT t1 _ t2 -> go s f t1 *> go s f t2 + ParensT t -> go s f t +#if MIN_VERSION_template_haskell(2,15,0) + AppKindT t k -> go s f t *> go s f k + ImplicitParamT _ t -> go s f t +#endif + _ -> pure () + -- | Substitute using a map of names in for /free/ type variables substTypeVars :: HasTypeVars t => Map Name Name -> t -> t substTypeVars m = over typeVars $ \n -> fromMaybe n (n `Map.lookup` m) @@ -89,11 +120,15 @@ substType m t@(VarT n) = fromMaybe t (n `Map.lookup` m) substType m (ForallT bs ctx ty) = ForallT bs (substType m' ctx) (substType m' ty) where m' = foldrOf typeVars Map.delete m bs - substType m (SigT t k) = SigT (substType m t) k + substType m (SigT t k) = SigT (substType m t) (substType m k) substType m (AppT l r) = AppT (substType m l) (substType m r) substType m (InfixT t1 n t2) = InfixT (substType m t1) n (substType m t2) substType m (UInfixT t1 n t2) = UInfixT (substType m t1) n (substType m t2) substType m (ParensT t) = ParensT (substType m t) +#if MIN_VERSION_template_haskell(2,15,0) + substType m (AppKindT t k) = AppKindT (substType m t) (substType m k) + substType m (ImplicitParamT n t) = ImplicitParamT n (substType m t) +#endif substType _ t = t instance SubstType t => SubstType [t] where diff --git a/src/Optics/TH.hs b/src/Optics/TH.hs --- a/src/Optics/TH.hs +++ b/src/Optics/TH.hs @@ -110,15 +110,15 @@ -- -- @ -- instance --- (a ~ Int, b ~ Int --- ) => LabelOptic "age" A_Lens Animal Animal a b where +-- (k ~ A_Lens, a ~ Int, b ~ Int +-- ) => LabelOptic "age" k Animal Animal a b where -- labelOptic = lensVL $ \\f s -> case s of -- Cat x1 x2 -> fmap (\\y -> Cat y x2) (f x1) -- Dog x1 x2 -> fmap (\\y -> Dog y x2) (f x1) -- -- instance --- (a ~ String, b ~ String --- ) => LabelOptic "name" An_AffineTraversal Animal Animal a b where +-- (k ~ An_AffineTraversal, a ~ String, b ~ String +-- ) => LabelOptic "name" k Animal Animal a b where -- labelOptic = atraversalVL $ \\point f s -> case s of -- Cat x1 x2 -> fmap (\\y -> Cat x1 y) (f x2) -- Dog x1 x2 -> point (Dog x1 x2) @@ -169,8 +169,8 @@ -- @ -- data Dog = Dog String Int -- deriving Show --- instance LabelOptic "name" A_Lens Dog Dog ... --- instance LabelOptic "age" A_Lens Dog Dog ... +-- instance (k ~ A_Lens, ...) => LabelOptic "name" k Dog Dog ... +-- instance (k ~ A_Lens, ...) => LabelOptic "age" k Dog Dog ... -- @ declareFieldLabels :: DecsQ -> DecsQ declareFieldLabels diff --git a/src/Optics/TH/Internal/Product.hs b/src/Optics/TH/Internal/Product.hs --- a/src/Optics/TH/Internal/Product.hs +++ b/src/Optics/TH/Internal/Product.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE BangPatterns #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE LambdaCase #-} @@ -72,11 +73,11 @@ makeFieldOpticsForDatatype :: LensRules -> D.DatatypeInfo -> HasFieldClasses [Dec] makeFieldOpticsForDatatype rules info = do perDef <- lift $ do - fieldCons <- traverse normalizeConstructor cons + fieldCons <- traverse (normalizeConstructor info) cons let allFields = toListOf (folded % _2 % folded % _1 % folded) fieldCons let defCons = over normFieldLabels (expandName allFields) fieldCons allDefs = setOf (normFieldLabels % folded) defCons - T.sequenceA (M.fromSet (buildScaffold True rules s defCons) allDefs) + T.sequenceA (M.fromSet (buildScaffold False rules s defCons) allDefs) let defs = M.toList perDef case _classyLenses rules tyName of @@ -87,7 +88,7 @@ where tyName = D.datatypeName info - s = D.datatypeType info + s = addKindVars info $ D.datatypeType info cons = D.datatypeCons info -- Traverse the field labels of a normalized constructor @@ -110,11 +111,11 @@ makeFieldLabelsForDatatype :: LensRules -> D.DatatypeInfo -> Q [Dec] makeFieldLabelsForDatatype rules info = do perDef <- do - fieldCons <- traverse normalizeConstructor cons + fieldCons <- traverse (normalizeConstructor info) cons let allFields = toListOf (folded % _2 % folded % _1 % folded) fieldCons let defCons = over normFieldLabels (expandName allFields) fieldCons allDefs = setOf (normFieldLabels % folded) defCons - T.sequenceA (M.fromSet (buildScaffold False rules s defCons) allDefs) + T.sequenceA (M.fromSet (buildScaffold True rules s defCons) allDefs) let defs = filter isRank1 $ M.toList perDef traverse (makeFieldLabel rules) defs @@ -123,11 +124,11 @@ -- LabelOptic doesn't support higher rank fields because of functional -- dependencies (s -> a, t -> b), so just skip them. isRank1 = \case - (_, (OpticSa rank1 _ _ _ _, _)) -> rank1 - _ -> True + (_, (OpticSa vs _ _ _ _, _)) -> null vs + _ -> True tyName = D.datatypeName info - s = D.datatypeType info + s = addKindVars info $ D.datatypeType info cons = D.datatypeCons info -- Traverse the field labels of a normalized constructor @@ -145,21 +146,17 @@ makeFieldLabel rules (defName, (defType, cons)) = do (context, instHead) <- case defType of OpticSa _ _ otype s a -> do + (k, cxtK) <- eqSubst (ConT $ opticTypeToTag otype) "k" (a', cxtA) <- eqSubst a "a" (b', cxtB) <- eqSubst a "b" - pure (pure [cxtA, cxtB], pure $ conAppsT ''LabelOptic - [LitT (StrTyLit fieldName), ConT $ opticTypeToTag otype, s, s, a', b']) + pure (pure [cxtK, cxtA, cxtB], pure $ conAppsT ''LabelOptic + [LitT (StrTyLit fieldName), k, s, s, a', b']) OpticStab otype s t a b -> do - ambiguousTypeFamilies <- containsAmbiguousTypeFamilyApplications s a - -- If 'a' contains ambiguous type family applications, generate type - -- preserving version as functional dependencies on LabelOptic demand it. - let t' = if ambiguousTypeFamilies then s else t + (k, cxtK) <- eqSubst (ConT $ opticTypeToTag otype) "k" (a', cxtA) <- eqSubst a "a" - (b', cxtB) <- if ambiguousTypeFamilies - then eqSubst a "b" - else eqSubst b "b" - pure (pure [cxtA, cxtB], pure $ conAppsT ''LabelOptic - [LitT (StrTyLit fieldName), ConT $ opticTypeToTag otype, s, t', a', b']) + (b', cxtB) <- eqSubst b "b" + pure (pure [cxtK, cxtA, cxtB], pure $ conAppsT ''LabelOptic + [LitT (StrTyLit fieldName), k, s, t, a', b']) instanceD context instHead (fun 'labelOptic) where opticTypeToTag AffineFoldType = ''An_AffineFold @@ -170,18 +167,6 @@ opticTypeToTag LensType = ''A_Lens opticTypeToTag TraversalType = ''A_Traversal - -- TODO: check for injectivity of encountered type families. - containsAmbiguousTypeFamilyApplications s a = do - -- We consider type family application ambiguous only if it's applied to a - -- type variable not referenced anywhere else. - (hasTypeFamilies, bareVars) <- (`runStateT` setOf typeVars s) $ - go =<< lift (D.resolveTypeSynonyms a) - pure $ hasTypeFamilies && not (S.null bareVars) - where - go (ConT nm) = has (_FamilyI % _1 % _TypeFamilyD) <$> lift (reify nm) - go (VarT n) = modify' (S.delete n) *> pure False - go ty = or <$> traverse go (toListOf typeSelf ty) - fieldName = case defName of TopName fname -> nameBase fname MethodName _ fname -> nameBase fname @@ -196,10 +181,11 @@ -- eliminating the variance between records, infix constructors, and normal -- constructors. normalizeConstructor :: + D.DatatypeInfo -> D.ConstructorInfo -> Q (Name, [(Maybe Name, Type)]) -- ^ constructor name, field name, field type -normalizeConstructor con = +normalizeConstructor info con = return (D.constructorName con, zipWith checkForExistentials fieldNames (D.constructorFields con)) where @@ -213,41 +199,41 @@ -- elligible for TH generated optics. checkForExistentials _ fieldtype | any (\tv -> D.tvName tv `S.member` used) unallowable - = (Nothing, fieldtype) + = (Nothing, addKindVars info fieldtype) where used = setOf typeVars fieldtype unallowable = D.constructorVars con - checkForExistentials fieldname fieldtype = (fieldname, fieldtype) + checkForExistentials fieldname fieldtype = (fieldname, addKindVars info fieldtype) -- | Compute the positional location of the fields involved in -- each constructor for a given optic definition as well as the -- type of clauses to generate and the type to annotate the declaration -- with. buildScaffold :: - Bool {- ^ allow change of phantom type parameters -} -> + Bool {- ^ for class instance? -} -> LensRules -> Type {- ^ outer type -} -> [(Name, [([DefName], Type)])] {- ^ normalized constructors -} -> DefName {- ^ target definition -} -> Q (OpticStab, [(Name, Int, [Int])]) {- ^ optic type, definition type, field count, target fields -} -buildScaffold allowPhantomsChange rules s cons defName = +buildScaffold forClassInstance rules s cons defName = - do (s',t,a,b) <- buildStab allowPhantomsChange s (concatMap snd consForDef) + do (s',t,a,b) <- buildStab forClassInstance s (concatMap snd consForDef) let defType - | Just (tyvars,cx,a') <- preview _ForallT a = + | Just (tyvars, cx, a') <- preview _ForallT a = let optic | lensCase = GetterType | affineCase = AffineFoldType | otherwise = FoldType - in OpticSa (null tyvars) cx optic s' a' + in OpticSa tyvars cx optic s' a' -- Getter and Fold are always simple | not (_allowUpdates rules) = let optic | lensCase = GetterType | affineCase = AffineFoldType | otherwise = FoldType - in OpticSa True [] optic s' a + in OpticSa [] [] optic s' a -- Generate simple Lens and Traversal where possible | _simpleLenses rules || s' == t && a == b = @@ -255,7 +241,7 @@ | lensCase = LensType | affineCase = AffineTraversalType | otherwise = TraversalType - in OpticSa True [] optic s' a + in OpticSa [] [] optic s' a -- Generate type-changing Lens and Traversal otherwise | otherwise = @@ -324,14 +310,16 @@ then ''Traversal else ''Traversal' -data OpticStab = OpticStab OpticType Type Type Type Type - | OpticSa Bool Cxt OpticType Type Type +data OpticStab + = OpticStab OpticType Type Type Type Type + | OpticSa [TyVarBndr] Cxt OpticType Type Type + deriving Show stabToType :: OpticStab -> Type -stabToType (OpticStab c s t a b) = - quantifyType [] (opticTypeName True c `conAppsT` [s,t,a,b]) -stabToType (OpticSa _ cx c s a ) = - quantifyType cx (opticTypeName False c `conAppsT` [s,a]) +stabToType (OpticStab c s t a b) = + quantifyType [] [] (opticTypeName True c `conAppsT` [s,t,a,b]) +stabToType (OpticSa vs cx c s a) = + quantifyType vs cx (opticTypeName False c `conAppsT` [s,a]) stabToContext :: OpticStab -> Cxt stabToContext OpticStab{} = [] @@ -358,9 +346,9 @@ -- These types are "raw" and will be packaged into an 'OpticStab' -- shortly after creation. buildStab :: Bool -> Type -> [Either Type Type] -> Q (Type,Type,Type,Type) -buildStab allowPhantomsChange s categorizedFields = do +buildStab forClassInstance s categorizedFields = do -- compute possible type changes - sub <- T.sequenceA (M.fromSet (newName . nameBase) unfixedTypeVars) + sub <- T.sequenceA . M.fromSet (newName . nameBase) =<< unfixedTypeVars let (t, b) = over each (substTypeVars sub) (s, a) pure (s, t, a, b) where @@ -374,12 +362,79 @@ in setOf typeVars s S.\\ setOf allTypeVars categorizedFields (fixedFields, targetFields) = partitionEithers categorizedFields - unfixedTypeVars = - let fixedTypeVars = setOf typeVars fixedFields - in if allowPhantomsChange - then setOf typeVars s S.\\ fixedTypeVars - else setOf typeVars s S.\\ fixedTypeVars S.\\ phantomTypeVars + unfixedTypeVars + | forClassInstance = do + ambiguousTypeVars <- getAmbiguousTypeFamilyTypeVars + --runIO $ do + -- putStrLn $ "S: " ++ show s + -- putStrLn $ "A: " ++ show a + -- putStrLn $ "FREE: " ++ show freeTypeVars + -- putStrLn $ "FIXED: " ++ show fixedTypeVars + -- putStrLn $ "PHANTOM: " ++ show phantomTypeVars + -- putStrLn $ "AMBIGUOUS: " ++ show ambiguousTypeVars + pure $ freeTypeVars S.\\ fixedTypeVars + S.\\ phantomTypeVars + S.\\ ambiguousTypeVars + | otherwise = pure $ freeTypeVars S.\\ fixedTypeVars + where + freeTypeVars = setOf typeVars s + fixedTypeVars = setOf typeVars fixedFields + + getAmbiguousTypeFamilyTypeVars = do + a' <- D.resolveTypeSynonyms a + execStateT (go a') $ setOf typeVars a' + where + go :: Type -> StateT (S.Set Name) Q (Maybe (Int, TypeFamilyHead, [Type])) + go (ForallT _ _ ty) = go ty + go (ParensT ty) = go ty + go (SigT ty kind) = go ty *> go kind + go (InfixT ty1 nm ty2) = procInfix ty1 nm ty2 *> pure Nothing + go (UInfixT ty1 nm ty2) = procInfix ty1 nm ty2 *> pure Nothing + + go (VarT n) = modify' (S.delete n) *> pure Nothing + + -- If type family is encountered, descend down and collect all of its + -- arguments for processing. + go (ConT nm) = do + let getVarLen tf@(TypeFamilyHead _ varBndrs _ _) = (length varBndrs, tf, []) + preview (_FamilyI % _1 % typeFamilyHead % to getVarLen) <$> lift (reify nm) + + go (AppT ty1 ty2) = go ty1 >>= \case + Just (n, tf, !args) + | n > 1 -> pure $ Just (n - 1, tf, ty2 : args) + | n == 1 -> procTF tf (reverse $ ty2 : args) *> pure Nothing + | otherwise -> error "go: unreachable" + Nothing -> go ty2 + + go _ = pure Nothing + + procInfix ty1 nm ty2 = do + mtf <- preview (_FamilyI % _1 % typeFamilyHead) <$> lift (reify nm) + case mtf of + Just tf -> procTF tf [ty1, ty2] + Nothing -> go ty1 *> go ty2 *> pure () + + -- Once fully applied type family is collected, the only arguments that + -- should be traversed further are these with injectivity annotation. + procTF :: TypeFamilyHead -> [Type] -> StateT (S.Set Name) Q () + procTF tf args = case tf of + TypeFamilyHead _ varBndrs _ (Just (InjectivityAnn _ ins)) -> do + let insSet = S.fromList ins + vars = map bndrName varBndrs + --lift . runIO $ do + -- putStrLn $ "INS: " ++ show ins + -- putStrLn $ "VARS: " ++ show vars + -- putStrLn $ "ARGS: " ++ show args + forM_ (sameLenZip vars args) $ \(var, arg) -> + when (var `S.member` insSet) . void $ go arg + _ -> pure () + where + sameLenZip (x : xs) (y : ys) = (x, y) : sameLenZip xs ys + sameLenZip [] [] = [] + sameLenZip _ _ = error "sameLenZip: different lengths" + + -- | Build the signature and definition for a single field optic. -- In the case of a singleton constructor irrefutable matches are -- used to enable the resulting lenses to be used on a bottom value. @@ -460,6 +515,7 @@ | (TopName defName, (stab, _)) <- defs , let body = infixApp (varE methodName) (varE '(%)) (varE defName) , let ty = quantifyType' (S.fromList (c:vars)) + [] (stabToContext stab) $ stabToOptic stab `conAppsT` [VarT c, stabToA stab] @@ -497,6 +553,7 @@ [sigD methodName (return methodType)] where methodType = quantifyType' (S.fromList [s,a]) + [] (stabToContext defType) $ stabToOptic defType `conAppsT` [VarT s,VarT a] s = mkName "s" @@ -514,7 +571,7 @@ containsTypeFamilies = go <=< D.resolveTypeSynonyms where - go (ConT nm) = has (_FamilyI % _1 % _TypeFamilyD) <$> reify nm + go (ConT nm) = has (_FamilyI % _1 % typeFamilyHead) <$> reify nm go ty = or <$> traverse go (toListOf typeSelf ty) pickInstanceDec hasFamilies @@ -795,7 +852,7 @@ -- | Name to give to generated field optics. data DefName - = TopName Name -- ^ Simple top-level definiton name + = TopName Name -- ^ Simple top-level definition name | MethodName Name Name -- ^ makeFields-style class name and method name deriving (Show, Eq, Ord) @@ -818,21 +875,6 @@ -- Miscellaneous utility functions ------------------------------------------------------------------------ - -- We want to catch type families, but not *data* families. See #799. -_TypeFamilyD :: AffineFold Dec () -_TypeFamilyD = _OpenTypeFamilyD % united `afailing` _ClosedTypeFamilyD % united - --- | Template Haskell wants type variables declared in a forall, so --- we find all free type variables in a given type and declare them. -quantifyType :: Cxt -> Type -> Type -quantifyType = quantifyType' S.empty - --- | This function works like 'quantifyType' except that it takes --- a list of variables to exclude from quantification. -quantifyType' :: S.Set Name -> Cxt -> Type -> Type -quantifyType' exclude c t = ForallT vs c t - where - vs = map PlainTV - $ filter (`S.notMember` exclude) - $ nub -- stable order - $ toListOf typeVars t +-- We want to catch type families, but not *data* families. See #799. +typeFamilyHead :: AffineFold Dec TypeFamilyHead +typeFamilyHead = _OpenTypeFamilyD `afailing` _ClosedTypeFamilyD % _1 diff --git a/src/Optics/TH/Internal/Sum.hs b/src/Optics/TH/Internal/Sum.hs --- a/src/Optics/TH/Internal/Sum.hs +++ b/src/Optics/TH/Internal/Sum.hs @@ -83,7 +83,7 @@ makePrismLabels :: Name -> DecsQ makePrismLabels typeName = do info <- D.reifyDatatype typeName - let cons = map normalizeCon $ D.datatypeCons info + let cons = map (normalizeCon info) $ D.datatypeCons info catMaybes <$> traverse (makeLabel info cons) cons where makeLabel :: D.DatatypeInfo -> [NCon] -> NCon -> Q (Maybe Dec) @@ -94,14 +94,17 @@ -- into OpticLabel because of functional dependencies, just skip them. ReviewType -> pure Nothing _ -> do + (k, cxtK) <- eqSubst (ConT $ opticTypeToTag otype) "k" (a', cxtA) <- eqSubst a "a" (b', cxtB) <- eqSubst b "b" let label = nameBase . prismName $ view nconName con instHead = pure $ conAppsT ''LabelOptic - [LitT (StrTyLit label), ConT $ opticTypeToTag otype, s, t, a', b'] - Just <$> instanceD (pure $ cx ++ [cxtA, cxtB]) instHead (fun stab 'labelOptic) + [LitT (StrTyLit label), k, s, t, a', b'] + Just <$> instanceD (pure $ cx ++ [cxtK, cxtA, cxtB]) + instHead + (fun stab 'labelOptic) where - ty = D.datatypeType info + ty = addKindVars info $ D.datatypeType info isNewtype = D.datatypeVariant info == D.Newtype opticTypeToTag IsoType = ''An_Iso @@ -123,7 +126,7 @@ let cls | normal = Nothing | otherwise = Just (D.datatypeName info) cons = D.datatypeCons info - makeConsPrisms info (map normalizeCon cons) cls + makeConsPrisms info (map (normalizeCon info) cons) cls -- | Generate prisms for the given 'Dec' @@ -133,7 +136,7 @@ let cls | normal = Nothing | otherwise = Just (D.datatypeName info) cons = D.datatypeCons info - makeConsPrisms info (map normalizeCon cons) cls + makeConsPrisms info (map (normalizeCon info) cons) cls -- | Generate prisms for the given type, normalized constructors, and an -- optional name to be used for generating a prism class. This function @@ -149,11 +152,11 @@ then varE 'coerced else makeConOpticExp stab cons con sequenceA $ - [ sigD n (close (stabToType stab)) + [ sigD n . pure . close $ stabToType stab , valD (varP n) (normalB body) [] ] ++ inlinePragma n where - ty = D.datatypeType info + ty = addKindVars info $ D.datatypeType info isNewtype = D.datatypeVariant info == D.Newtype -- classy prism class and instance @@ -213,9 +216,9 @@ ReviewType -> ''Review `conAppsT` [t,b] where - vs = map PlainTV - $ nub -- stable order - $ toListOf typeVars cx + vs = D.freeVariablesWellScoped + . S.toList + $ setOf (folded % typeVarsKinded) cx stabType :: Stab -> OpticType stabType (Stab _ o _ _ _ _) = o @@ -236,21 +239,30 @@ -- | Compute the full type-changing Prism type given an outer type, list of -- constructors, and target constructor name. computePrismType :: StabConfig -> Type -> Cxt -> [NCon] -> NCon -> Q Stab -computePrismType conf t cx cons con = do +computePrismType conf s cx cons con = do let ts = view nconTypes con + free = setOf typeVars s fixed = setOf typeVars cons - phantoms = setOf typeVars t S.\\ (setOf typeVars con `S.union` fixed) + phantoms = free S.\\ setOf (folded % nconTypes % typeVars) (con : cons) unbound = if scAllowPhantomsChange conf - then setOf typeVars t S.\\ fixed - else setOf typeVars t S.\\ fixed S.\\ phantoms + then free S.\\ fixed + else free S.\\ fixed S.\\ phantoms sub <- sequenceA (M.fromSet (newName . nameBase) unbound) - b <- toTupleT (map return ts) - a <- toTupleT (map return (substTypeVars sub ts)) - let s = substTypeVars sub t + a <- toTupleT (map return ts) + b <- toTupleT (map return (substTypeVars sub ts)) + --runIO $ do + -- putStrLn $ "S: " ++ show s + -- putStrLn $ "A: " ++ show a + -- putStrLn $ "FREE: " ++ show free + -- putStrLn $ "FIXED: " ++ show fixed + -- putStrLn $ "PHANTOMS: " ++ show phantoms + -- putStrLn $ "UNBOUND: " ++ show unbound + let t = substTypeVars sub s + cx' = substTypeVars sub cx otype = if null cons && scAllowIsos conf then IsoType else PrismType - return (Stab cx otype s t a b) + return (Stab cx' otype s t a b) -- | Construct either a Review or Prism as appropriate makeConOpticExp :: Stab -> [NCon] -> NCon -> ExpQ @@ -322,9 +334,9 @@ -- | Construct the remit portion of a prism. -- Pattern match only target constructor, no type changing -- --- (\x -> case s of +-- (\s -> case s of -- Con x y z -> Right (x,y,z) --- _ -> Left x +-- _ -> Left s -- ) :: s -> Either s a makeSimpleRemitter :: Name -> Int -> ExpQ makeSimpleRemitter conName fields = @@ -341,7 +353,7 @@ -- | Pattern match all constructors to enable type-changing -- --- (\x -> case s of +-- (\s -> case s of -- Con x y z -> Right (x,y,z) -- Other_n w -> Left (Other_n w) -- ) :: s -> Either t a @@ -474,11 +486,11 @@ -- | Normalize a single 'Con' to its constructor name and field types. -normalizeCon :: D.ConstructorInfo -> NCon -normalizeCon info = NCon (D.constructorName info) - (D.tvName <$> D.constructorVars info) - (D.constructorContext info) - (D.constructorFields info) +normalizeCon :: D.DatatypeInfo -> D.ConstructorInfo -> NCon +normalizeCon di info = NCon (D.constructorName info) + (D.tvName <$> D.constructorVars info) + (D.constructorContext info) + (map (addKindVars di) $ D.constructorFields info) -- | Compute a prism's name by prefixing an underscore for normal @@ -491,7 +503,6 @@ -- | Quantify all the free variables in a type. -close :: Type -> TypeQ -close t = forallT (map PlainTV (S.toList vs)) (cxt[]) (return t) - where - vs = setOf typeVars t +close :: Type -> Type +close (ForallT vars cx ty) = quantifyType vars cx ty +close ty = quantifyType [] [] ty diff --git a/src/Optics/TH/Internal/Utils.hs b/src/Optics/TH/Internal/Utils.hs --- a/src/Optics/TH/Internal/Utils.hs +++ b/src/Optics/TH/Internal/Utils.hs @@ -1,8 +1,15 @@ module Optics.TH.Internal.Utils where +import Data.Maybe import Language.Haskell.TH +import qualified Data.Map as M +import qualified Data.Set as S import qualified Language.Haskell.TH.Datatype as D +import Data.Set.Optics +import Language.Haskell.TH.Optics.Internal +import Optics.Core + -- | Apply arguments to a type constructor appsT :: TypeQ -> [TypeQ] -> TypeQ appsT = foldl appT @@ -48,6 +55,31 @@ placeholder <- VarT <$> newName n pure (placeholder, D.equalPred placeholder ty) +-- | Fill in kind variables using info from datatype type parameters. +addKindVars :: D.DatatypeInfo -> Type -> Type +addKindVars = substType . M.fromList . mapMaybe var . D.datatypeInstTypes + where + var t@(SigT (VarT n) k) + | has typeVars k = Just (n, t) + | otherwise = Nothing + var _ = Nothing + +-- | Template Haskell wants type variables declared in a forall, so +-- we find all free type variables in a given type and declare them. +quantifyType :: [TyVarBndr] -> Cxt -> Type -> Type +quantifyType = quantifyType' S.empty + +-- | This function works like 'quantifyType' except that it takes +-- a list of variables to exclude from quantification. +quantifyType' :: S.Set Name -> [TyVarBndr] -> Cxt -> Type -> Type +quantifyType' exclude vars cx t = ForallT vs cx t + where + vs = filter (\v -> bndrName v `S.notMember` exclude) + . D.freeVariablesWellScoped + $ map bndrToType vars ++ S.toList (setOf typeVarsKinded t) + + bndrToType (PlainTV n) = VarT n + bndrToType (KindedTV n k) = SigT (VarT n) k ------------------------------------------------------------------------ -- Support for generating inline pragmas diff --git a/tests/Optics/TH/Tests.hs b/tests/Optics/TH/Tests.hs --- a/tests/Optics/TH/Tests.hs +++ b/tests/Optics/TH/Tests.hs @@ -3,13 +3,20 @@ {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE OverloadedLabels #-} +{-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeFamilyDependencies #-} +{-# LANGUAGE TypeInType #-} +{-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} -- {-# OPTIONS_GHC -ddump-splices #-} module Main where +import Data.Functor.Const +import Data.Kind (Type) +import Data.Tagged import Data.Typeable import Optics.Core @@ -135,6 +142,53 @@ checkClassyT3 :: AsClassyTest r => Prism' r Char checkClassyT3 = _ClassyT3 +data WeirdThing (a :: k -> Type) (b :: k -> Type) = WeirdThing +data Weird1 a b = Weird1 (WeirdThing a (Const b)) +makePrisms ''Weird1 +makePrismLabels ''Weird1 + +checkWeird1 :: Iso (Weird1 a b ) + (Weird1 a' b') + (WeirdThing a (Const b)) + (WeirdThing a' (Const b')) +checkWeird1 = _Weird1 + +checkWeird1_ :: Iso (Weird1 a b ) + (Weird1 a' b') + (WeirdThing a (Const b)) + (WeirdThing a' (Const b')) +checkWeird1_ = #_Weird1 + +data Weird2 (a :: k -> Type) (b :: k -> Type) where + Weird2 :: Weird2 (a :: Type -> Type) b +makePrisms ''Weird2 +makePrismLabels ''Weird2 + +checkWeird2 + :: forall k (a :: k -> Type) + (b :: k -> Type) + (a' :: Type -> Type) + (b' :: Type -> Type) + . Iso (Weird2 a b) (Weird2 a' b') () () +checkWeird2 = _Weird2 + +checkWeird2_ + :: forall (a :: Type -> Type) + (b :: Type -> Type) + . Iso (Weird2 a b) (Weird2 a b) () () +checkWeird2_ = #_Weird2 + +data Weird3 (a :: k) where + Weird3 :: Weird3 (a :: Type) +makePrisms ''Weird3 +makePrismLabels ''Weird3 + +checkWeird3 :: forall k (a :: k) (b :: Type). Iso (Weird3 a) (Weird3 b) () () +checkWeird3 = _Weird3 + +checkWeird3_ :: forall (a :: Type). Iso (Weird3 a) (Weird3 a) () () +checkWeird3_ = #_Weird3 + ---------------------------------------- data Bar a b c = Bar { _baz :: (a, b) } @@ -449,14 +503,104 @@ checkThing2_ :: Lens (Lebowski a) (Lebowski b) (Maybe a) (Maybe b) checkThing2_ = #thing -type family Fam a +data Kinded0 k = Kinded0 + { _kinded0Thing :: forall a. Proxy (a :: k) + } +makeLenses ''Kinded0 + +checkKinded0Thing :: Getter (Kinded0 k) (Proxy (a :: k)) +checkKinded0Thing = kinded0Thing + +data Kinded1 (a :: k1) (b :: k2) = Kinded + { _kinded1Thing :: Tagged '(a, b) Int + } +makeFieldLabels ''Kinded1 + +checkKinded1Thing :: Iso (Kinded1 (a :: k1 ) (b :: k2 )) + (Kinded1 (a' :: k1') (b' :: k2')) + (Tagged '(a , b ) Int) + (Tagged '(a', b') Int) +checkKinded1Thing = #thing + +data Kinded2 k a = Kinded2 + { _kinded2Thing :: Proxy (a :: k) + } +makeFieldLabels ''Kinded2 + +checkKinded2Thing :: Iso (Kinded2 k a ) + (Kinded2 k' a') + (Proxy (a :: k )) + (Proxy (a' :: k')) +checkKinded2Thing = #thing + +type family Fam (a :: k) type instance Fam Int = String +-- unambiguous type family application data FamRec1 a = FamRec1 { _famRec1Thing :: a -> Fam a } makeFieldLabels ''FamRec1 checkFamRec1Thing :: Iso (FamRec1 a) (FamRec1 b) (a -> Fam a) (b -> Fam b) checkFamRec1Thing = #thing + +type family FamInj1 (a :: k) b = r | r -> a + +-- type family injective in its first parameter +data FamRec2 a b = FamRec2 { _famRec2Thing :: FamInj1 a b } +makeFieldLabels ''FamRec2 + +checkFamRec2Thing :: Iso (FamRec2 a b) (FamRec2 a' b) (FamInj1 a b) (FamInj1 a' b) +checkFamRec2Thing = #thing + +type family a :#: b = r | r -> b + +-- infix type family injective in its second parameter +data FamRec3 a b = FamRec3 { _famRec3Thing :: a :#: b } +makeFieldLabels ''FamRec3 + +checkFamRec3Thing :: Iso (FamRec3 a b) (FamRec3 a b') (a :#: b) (a :#: b') +checkFamRec3Thing = #thing + +-- ambiguous type family application, type-preserving optic +data FamRec4 a = FamRec4 { _famRec4Thing :: FamInj1 (Fam a) a } +makeFieldLabels ''FamRec4 -- no error + +-- no type changing optic here +checkFamRec4Thing :: Iso' (FamRec4 a) (FamInj1 (Fam a) a) +checkFamRec4Thing = #thing + +type family FamInj2 a b (c :: k) = r | r -> a b c + +-- poly kinded shenenigans +data FamRec5 a b (c :: k) = FamRec5 { _famRec5Thing :: FamInj2 a b '[c] } +makeFieldLabels ''FamRec5 + +-- type-changing, kind-changing optic +checkFamRec5Thing :: Iso (FamRec5 a b (c :: k )) + (FamRec5 a' b' (c' :: k')) + (FamInj2 a b '[c ]) + (FamInj2 a' b' '[c']) +checkFamRec5Thing = #thing + +-- ambiguous type family application + Tagged = type-changing optic +data FamRec6 a = FamRec6 { _famRec6Thing :: Tagged a (Fam a) } +makeFieldLabels ''FamRec6 + +checkFamRec6Thing + :: Iso (FamRec6 a) (FamRec6 b) (Tagged a (Fam a)) (Tagged b (Fam b)) +checkFamRec6Thing = #thing + +-- nested injective type family application + kind polymorphism +data FamRec7 a b (c :: [k]) = FamRec7 + { _famRec7Thing :: FamInj1 (b :#: (a -> FamInj1 c b)) b + } +makeFieldLabels ''FamRec7 + +checkFamRec7Thing :: Iso (FamRec7 a b (c :: [k ])) + (FamRec7 a' b (c' :: [k'])) + (FamInj1 (b :#: (a -> FamInj1 c b)) b) + (FamInj1 (b :#: (a' -> FamInj1 c' b)) b) +checkFamRec7Thing = #thing data FamRec a = FamRec { _famRecThing :: Fam a