Commit 1acb922b authored by David Feuer's avatar David Feuer Committed by David Feuer

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
parent bc761ad9
......@@ -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.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment