Make the Con and Con' patterns produce evidence

Matching with the `Con` and `Con'` patterns can reveal evidence
that the type in question is *not* an application. This can help
the pattern checker.

Reviewers: austin, hvr, bgamari

Reviewed By: bgamari

Subscribers: carter, rwbarton, thomie

Differential Revision: https://phabricator.haskell.org/D4139

1 files changed, 56 insertions, 13 deletions

diff --git a/libraries/base/Data/Typeable/Internal.hs b/libraries/base/Data/Typeable/Internal.hs
index d2ed9d1500..a01a9ff859 100644
--- a/libraries/base/Data/Typeable/Internal.hs
+++ b/libraries/base/Data/Typeable/Internal.hs
@@ -18,6 +18,7 @@
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
 
 -----------------------------------------------------------------------------
 -- |
@@ -87,7 +88,7 @@ import Data.Type.Equality
 import GHC.List ( splitAt, foldl' )
 import GHC.Word
 import GHC.Show
-import GHC.TypeLits ( KnownSymbol, symbolVal' )
+import GHC.TypeLits ( KnownSymbol, symbolVal', AppendSymbol )
 import GHC.TypeNats ( KnownNat, natVal' )
 import Unsafe.Coerce ( unsafeCoerce )
 
@@ -448,21 +449,32 @@ mkTrAppChecked a b = mkTrApp a b
 pattern App :: forall k2 (t :: k2). ()
             => forall k1 (a :: k1 -> k2) (b :: k1). (t ~ a b)
             => TypeRep a -> TypeRep b -> TypeRep t
-pattern App f x <- (splitApp -> Just (IsApp f x))
+pattern App f x <- (splitApp -> IsApp f x)
   where App f x = mkTrAppChecked f x
 
-data IsApp (a :: k) where
+data AppOrCon (a :: k) where
     IsApp :: forall k k' (f :: k' -> k) (x :: k'). ()
-          => TypeRep f -> TypeRep x -> IsApp (f x)
+          => TypeRep f -> TypeRep x -> AppOrCon (f x)
+    -- See Note [Con evidence]
+    IsCon :: IsApplication a ~ "" => TyCon -> [SomeTypeRep] -> AppOrCon a
+
+type family IsApplication (x :: k) :: Symbol where
+  IsApplication (_ _) = "An error message about this unifying with \"\" "
+     `AppendSymbol` "means that you tried to match a TypeRep with Con or "
+     `AppendSymbol` "Con' when the represented type was known to be an "
+     `AppendSymbol` "application."
+  IsApplication _ = ""
 
 splitApp :: forall k (a :: k). ()
          => TypeRep a
-         -> Maybe (IsApp a)
-splitApp TrType = Just (IsApp trTYPE trLiftedRep)
-splitApp (TrApp {trAppFun = f, trAppArg = x}) = Just (IsApp f x)
-splitApp rep@(TrFun {trFunArg=a, trFunRes=b}) = Just (IsApp (mkTrApp arr a) b)
+         -> AppOrCon a
+splitApp TrType = IsApp trTYPE trLiftedRep
+splitApp (TrApp {trAppFun = f, trAppArg = x}) = IsApp f x
+splitApp rep@(TrFun {trFunArg=a, trFunRes=b}) = IsApp (mkTrApp arr a) b
   where arr = bareArrow rep
-splitApp (TrTyCon{})                          = Nothing
+splitApp (TrTyCon{trTyCon = con, trKindVars = kinds})
+  = case unsafeCoerce Refl :: IsApplication a :~: "" of
+      Refl -> IsCon con kinds
 
 -- | Use a 'TypeRep' as 'Typeable' evidence.
 withTypeable :: forall (a :: k) (r :: TYPE rep). ()
@@ -475,8 +487,10 @@ withTypeable rep k = unsafeCoerce k' rep
 newtype Gift a (r :: TYPE rep) = Gift (Typeable a => r)
 
 -- | Pattern match on a type constructor
-pattern Con :: forall k (a :: k). TyCon -> TypeRep a
-pattern Con con <- TrTyCon {trTyCon = con}
+pattern Con :: forall k (a :: k). ()
+            => IsApplication a ~ "" -- See Note [Con evidence]
+            => TyCon -> TypeRep a
+pattern Con con <- (splitApp -> IsCon con _)
 
 -- | Pattern match on a type constructor including its instantiated kind
 -- variables.
@@ -495,13 +509,42 @@ pattern Con con <- TrTyCon {trTyCon = con}
 -- intRep     == typeRep @Int
 -- @
 --
-pattern Con' :: forall k (a :: k). TyCon -> [SomeTypeRep] -> TypeRep a
-pattern Con' con ks <- TrTyCon {trTyCon = con, trKindVars = ks}
+pattern Con' :: forall k (a :: k). ()
+             => IsApplication a ~ "" -- See Note [Con evidence]
+             => TyCon -> [SomeTypeRep] -> TypeRep a
+pattern Con' con ks <- (splitApp -> IsCon con ks)
 
 -- TODO: Remove Fun when #14253 is fixed
 {-# COMPLETE Fun, App, Con  #-}
 {-# COMPLETE Fun, App, Con' #-}
 
+{- Note [Con evidence]
+    ~~~~~~~~~~~~~~~~~~~
+
+Matching TypeRep t on Con or Con' fakes up evidence that
+
+  IsApplication t ~ "".
+
+Why should anyone care about the value of strange internal type family?
+Well, almost nobody cares about it, but the pattern checker does!
+For example, suppose we have TypeRep (f x) and we want to get
+TypeRep f and TypeRep x. There is no chance that the Con constructor
+will match, because (f x) is not a constructor, but without the
+IsApplication evidence, omitting it will lead to an incomplete pattern
+warning. With the evidence, the pattern checker will see that
+Con wouldn't typecheck, so everything works out as it should.
+
+Why do we use Symbols? We would really like to use something like
+
+  type family NotApplication (t :: k) :: Constraint where
+    NotApplication (f a) = TypeError ...
+    NotApplication _ = ()
+
+Unfortunately, #11503 means that the pattern checker and type checker
+will fail to actually reject the mistaken patterns. So we describe the
+error in the result type. It's a horrible hack.
+-}
+
 ----------------- Observation ---------------------
 
 -- | Observe the type constructor of a quantified type representation.