diff --git a/optics-core/src/Optics/Internal/Optic/Subtyping.hs b/optics-core/src/Optics/Internal/Optic/Subtyping.hs index 3b68dc6e..fccbb14b 100644 --- a/optics-core/src/Optics/Internal/Optic/Subtyping.hs +++ b/optics-core/src/Optics/Internal/Optic/Subtyping.hs @@ -1,15 +1,22 @@ {-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE UndecidableSuperClasses #-} {-# OPTIONS_HADDOCK not-home #-} -- | Instances to implement the subtyping hierarchy between optics. -- -- This module is intended for internal use only, and may change without warning -- in subsequent releases. -module Optics.Internal.Optic.Subtyping where +module Optics.Internal.Optic.Subtyping + ( Is(..) + , JoinKinds(..) + ) where +import Data.Kind (Constraint) +import Data.Type.Bool import GHC.TypeLits (ErrorMessage(..), TypeError) import Optics.Internal.Optic.TypeLevel @@ -32,13 +39,19 @@ instance Is k k where implies r = r -- | Overlappable instance for a custom type error. -instance {-# OVERLAPPABLE #-} TypeError - ('ShowType k ':<>: 'Text " cannot be used as " ':<>: 'ShowType l - ':$$: 'Text "Perhaps you meant one of these:" - ':$$: ShowEliminations (EliminationForms k) - ) => Is k l where +instance {-# OVERLAPPABLE #-} Isn't k l => Is k l where implies _ = error "unreachable" +-- | Hide the error message in a type family, for prettier Haddocks. (We can't +-- just use a type synonym, or use a class with a single instance, because then +-- GHC reports the 'TypeError' at the definition site.) +type family Isn't k l where + Isn't k l = + TypeError ('ShowType k ':<>: 'Text " cannot be used as " ':<>: 'ShowType l + ':$$: 'Text "Perhaps you meant one of these:" + ':$$: ShowEliminations (EliminationForms k) + ) + type family EliminationForms (k :: OpticKind) where EliminationForms An_AffineFold = AffineFoldEliminations EliminationForms An_AffineTraversal = AffineTraversalEliminations @@ -432,8 +445,95 @@ instance JoinKinds A_Setter A_Traversal A_Setter wher -- END GENERATED CONTENT +-- | Overlappable instance for a custom type error. instance {-# OVERLAPPABLE #-} ( JoinKinds k l m - , TypeError ('ShowType k ':<>: 'Text " cannot be composed with " ':<>: 'ShowType l) + , CannotJoinKinds k l m p v ) => JoinKinds k l m where joinKinds _ = error "unreachable" + + +-- | This type family is called when solving @JoinKinds k l m@ fails, with @p@ +-- and @v@ being fresh variables. It returns a constraint which, when solved, +-- displays a nice type error. +-- +-- We know that @k@ and @l@ must be concrete, because otherwise GHC would not +-- have committed to the OVERLAPPABLE instance above that uses CannotJoinKinds. +-- However @m@ may or may not be concrete, and we want to print a different +-- error in each case (#423). +-- +-- This could be a type synonym, except then GHC prints the type error at the +-- definition site of the type synonym, which is rather stupid. +-- +type family CannotJoinKinds k l m actual is_concrete :: Constraint where + CannotJoinKinds k l m actual is_concrete = + ( -- 1. Unify is_concrete with True or False + IsConcrete m is_concrete + -- 2. If is_concrete, unify actual with the join of k and m (otherwise + -- do nothing; the conditional is necessary to avoid an infinite + -- constraint solver loop). + , If is_concrete (JoinKinds k l actual) (() :: Constraint) + -- 3. Display an error that depends on is_concrete and actual + , TypeError (CannotJoinKindsMessage k l m actual is_concrete) + ) + +-- | If @is_concrete@ is True, then the context must be demanding an optic kind +-- that differs from the actual result of the composition (with the latter given +-- by the @actual@ parameter). For example: +-- +-- >>> :t castOptic @A_Setter @A_Setter (traversed % _1) +-- ... +-- ... • A_Traversal composed with A_Lens produces A_Traversal, +-- ... but the context expects A_Setter +-- ... +-- +-- Otherwise, the user has tried to compose two optic kinds that simply cannot +-- be used together, for example: +-- +-- >>> to not % mapped +-- ... +-- ... • A_Getter cannot be composed with A_Setter +-- ... +-- +type family CannotJoinKindsMessage k l m actual is_concrete where + CannotJoinKindsMessage k l m actual 'True + = 'ShowType k ':<>: 'Text " composed with " ':<>: 'ShowType l + ':<>: 'Text " produces " ':<>: 'ShowType actual ':<>: 'Text "," + ':$$: 'Text "but the context expects " ':<>: 'ShowType m + CannotJoinKindsMessage k l m actual 'False + = 'ShowType k ':<>: 'Text " cannot be composed with " ':<>: 'ShowType l + +-- | When solving an @IsConcrete m v@ constraint, if @m@ is concrete (i.e. a +-- type constructor) then @is_concrete@ will be unified with True; otherwise +-- (i.e. @m@ is a type variable or family application), @is_concrete@ will be +-- unified with @False@. +-- +-- Note that applications are considered as concrete, even if the head is a +-- variable. This means we get the following (but no user is likely to write +-- such nonsense): +-- +-- >>> castOptic @(_ _) (traversed % _1) +-- ... +-- ... • A_Traversal cannot be used as ... +-- ... +-- +type IsConcrete m is_concrete = IsConcreteHelper (PartialIsConcrete m) is_concrete + +-- | If @m@ is concrete, it is apart from 'Void0' and hence this will reduce to +-- True. Otherwise the family application gets stuck. +type family PartialIsConcrete m where + PartialIsConcrete Void0 = 'False + PartialIsConcrete _ = 'True + +-- | If the first parameter is True, unify the second parameter with True. If +-- the first parameter is anything else (crucially, including a stuck type +-- family application) unify the second parameter with False. +class IsConcreteHelper x is_concrete +instance is_concrete ~ 'True => IsConcreteHelper 'True is_concrete +instance {-# INCOHERENT #-} is_concrete ~ 'False => IsConcreteHelper f is_concrete + +-- | Non-exported, used solely to be apart from every other concrete type. +data Void0 + +-- $setup +-- >>> import Optics.Core