Improve error message for impossible JoinKinds constraint

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