content: {-# LANGUAGE TypeOperators #-}
  {-# LANGUAGE TypeFamilies #-}
  {-# LANGUAGE UndecidableInstances #-}
  
  {-# OPTIONS_GHC -Wall #-}
  
  -- | Bug(?) in Coercible constraint solving
  
  module T13083 where
  
  import Data.Kind
  import GHC.Generics (Par1(..),(:*:)(..))
  import GHC.Exts (coerce)
  
  -- Representation as free vector space
  type family V (a :: Type) :: Type -> Type
  
  type instance V R = Par1
  type instance V (a,b) = V a :*: V b
  
  type instance V (Par1 a) = V a
  
  data R = R
  
  -- Linear map in row-major order
  newtype L a b = L (V b (V a R))
  
  -- Use coerce to drop newtype wrapper
  bar :: L a b -> V b (V a R)
  bar = coerce
  
  {-
  [W] L a b ~R V b (V a R)
  -->
      V b (V a R)  ~R  V b (V a R)
  -}
  
  {--------------------------------------------------------------------
      Bug demo
  --------------------------------------------------------------------}
  
  -- A rejected type specialization of bar with a ~ (R,R), b ~ (Par1 R,R)
  foo :: L (R,R) (Par1 R,R) -> V (Par1 R,R) (V (R,R) R)
  -- foo :: L (a1,R) (Par1 b1,b2) -> V (Par1 b1,b2) (V (a1,R) R)
  foo = coerce
  
  {-
  [W] L (a1,R) (Par1 b1, b2)   ~R   V (Par1 b1,b2) (V (a1,R) R)
  -->
      V (Par1 b1, b2) (V (a1,R) R)  ~R    same
  
      -> (V (Par1 b1) :*: V b2) ((V a1 :*: V R) R)
      -> (:*:) (V b1) (V b2) (:*: (V a1) Par1 R)
  
  -->
      L (a1,R) (Par1 b1, b2)   ~R   (:*:) (V b1) (V b2) (:*: (V a1) Par1 R)
  -}
  
  --     • Couldn't match representation of type ‘V Par1’
  --                                with that of ‘Par1’
  --         arising from a use of ‘coerce’
  
  -- Note that Par1 has the wrong kind (Type -> Type) for V Par1
  
  -- Same error:
  --
  -- foo :: (a ~ (R,R), b ~ (Par1 R,R)) => L a b -> V b (V a R)
  
  -- The following similar signatures work:
  
  -- foo :: L (R,R) (R,Par1 R) -> V (R,Par1 R) (V (R,R) R)
  -- foo :: L (Par1 R,R) (R,R) -> V (R,R) (V (Par1 R,R) R)
  
  -- Same error:
  
  -- -- Linear map in column-major order
  -- newtype L a b = L (V a (V b s))
  
  -- foo :: L (R,R) (Par1 R,R) -> V (R,R) (V (Par1 R,R) R)
  -- foo = coerce
  
  