Add valid refinement substitution suggestions for typed holes
[ghc.git] / compiler / typecheck / TcEvidence.hs
index 2de2223..0930d7a 100644 (file)
@@ -13,11 +13,17 @@ module TcEvidence (
   -- Evidence bindings
   TcEvBinds(..), EvBindsVar(..),
   EvBindMap(..), emptyEvBindMap, extendEvBinds,
-  lookupEvBind, evBindMapBinds, foldEvBindMap, isEmptyEvBindMap,
+  lookupEvBind, evBindMapBinds, foldEvBindMap, filterEvBindMap,
+  isEmptyEvBindMap,
   EvBind(..), emptyTcEvBinds, isEmptyTcEvBinds, mkGivenEvBind, mkWantedEvBind,
   sccEvBinds, evBindVar,
-  EvTerm(..), mkEvCast, evVarsOfTerm, mkEvScSelectors,
-  EvLit(..), evTermCoercion,
+
+  -- EvTerm (already a CoreExpr)
+  EvTerm(..), EvExpr,
+  evId, evCoercion, evCast, evDFunApp,  evSelector,
+  mkEvCast, evVarsOfTerm, mkEvScSelectors, evTypeable, findNeededEvVars,
+
+  evTermCoercion,
   EvCallStack(..),
   EvTypeable(..),
 
@@ -33,12 +39,14 @@ module TcEvidence (
   mkTcKindCo,
   tcCoercionKind, coVarsOfTcCo,
   mkTcCoVarCo,
-  isTcReflCo,
+  isTcReflCo, isTcReflexiveCo,
   tcCoercionRole,
   unwrapIP, wrapIP
   ) where
 #include "HsVersions.h"
 
+import GhcPrelude
+
 import Var
 import CoAxiom
 import Coercion
@@ -54,15 +62,19 @@ import VarSet
 import Name
 import Pair
 
+import CoreSyn
+import Class ( classSCSelId )
+import Id ( isEvVar )
+import CoreFVs ( exprSomeFreeVars )
+
 import Util
 import Bag
 import Digraph
 import qualified Data.Data as Data
 import Outputable
-import FastString
 import SrcLoc
 import Data.IORef( IORef )
-import UniqFM
+import UniqSet
 
 {-
 Note [TcCoercions]
@@ -115,6 +127,10 @@ tcCoercionRole         :: TcCoercion -> Role
 coVarsOfTcCo           :: TcCoercion -> TcTyCoVarSet
 isTcReflCo             :: TcCoercion -> Bool
 
+-- | This version does a slow check, calculating the related types and seeing
+-- if they are equal.
+isTcReflexiveCo        :: TcCoercion -> Bool
+
 mkTcReflCo             = mkReflCo
 mkTcSymCo              = mkSymCo
 mkTcTransCo            = mkTransCo
@@ -143,7 +159,7 @@ tcCoercionKind         = coercionKind
 tcCoercionRole         = coercionRole
 coVarsOfTcCo           = coVarsOfCo
 isTcReflCo             = isReflCo
-
+isTcReflexiveCo        = isReflexiveCo
 
 {-
 %************************************************************************
@@ -299,11 +315,11 @@ mkWpCastN co
 mkWpTyApps :: [Type] -> HsWrapper
 mkWpTyApps tys = mk_co_app_fn WpTyApp tys
 
-mkWpEvApps :: [EvTerm] -> HsWrapper
-mkWpEvApps args = mk_co_app_fn WpEvApp args
+mkWpEvApps :: [EvExpr] -> HsWrapper
+mkWpEvApps args = mk_co_app_fn WpEvApp (map EvExpr args)
 
 mkWpEvVarApps :: [EvVar] -> HsWrapper
-mkWpEvVarApps vs = mk_co_app_fn WpEvApp (map EvId vs)
+mkWpEvVarApps vs = mk_co_app_fn WpEvApp (map (EvExpr . evId) vs)
 
 mkWpTyLams :: [TyVar] -> HsWrapper
 mkWpTyLams ids = mk_co_lam_fn WpTyLam ids
@@ -372,9 +388,11 @@ data EvBindsVar
       ebv_binds :: IORef EvBindMap,
       -- The main payload: the value-level evidence bindings
       --     (dictionaries etc)
+      -- Some Given, some Wanted
 
       ebv_tcvs :: IORef CoVarSet
       -- The free coercion vars of the (rhss of) the coercion bindings
+      -- All of these are Wanted
       --
       -- Coercions don't actually have bindings
       -- because we plug them in-place (via a mutable
@@ -434,6 +452,10 @@ evBindMapBinds = foldEvBindMap consBag emptyBag
 foldEvBindMap :: (EvBind -> a -> a) -> a -> EvBindMap -> a
 foldEvBindMap k z bs = foldDVarEnv k z (ev_bind_varenv bs)
 
+filterEvBindMap :: (EvBind -> Bool) -> EvBindMap -> EvBindMap
+filterEvBindMap k (EvBindMap { ev_bind_varenv = env })
+  = EvBindMap { ev_bind_varenv = filterDVarEnv k env }
+
 instance Outputable EvBindMap where
   ppr (EvBindMap m) = ppr m
 
@@ -452,72 +474,83 @@ evBindVar = eb_lhs
 mkWantedEvBind :: EvVar -> EvTerm -> EvBind
 mkWantedEvBind ev tm = EvBind { eb_is_given = False, eb_lhs = ev, eb_rhs = tm }
 
+-- EvTypeable are never given, so we can work with EvExpr here instead of EvTerm
+mkGivenEvBind :: EvVar -> EvExpr -> EvBind
+mkGivenEvBind ev tm = EvBind { eb_is_given = True, eb_lhs = ev, eb_rhs = EvExpr tm }
 
-mkGivenEvBind :: EvVar -> EvTerm -> EvBind
-mkGivenEvBind ev tm = EvBind { eb_is_given = True, eb_lhs = ev, eb_rhs = tm }
 
+-- An EvTerm is, conceptually, a CoreExpr that implements the constraint.
+-- Unfortunately, we cannot just do
+--   type EvTerm  = CoreExpr
+-- Because of staging problems issues around EvTypeable
 data EvTerm
-  = EvId EvId                    -- Any sort of evidence Id, including coercions
-
-  | EvCoercion TcCoercion        -- coercion bindings
-                                 -- See Note [Coercion evidence terms]
-
-  | EvCast EvTerm TcCoercionR    -- d |> co
+    = EvExpr EvExpr
+    | EvTypeable Type EvTypeable   -- Dictionary for (Typeable ty)
+  deriving Data.Data
 
-  | EvDFunApp DFunId             -- Dictionary instance application
-       [Type] [EvTerm]
+type EvExpr = CoreExpr
 
-  | EvDelayedError Type FastString  -- Used with Opt_DeferTypeErrors
-                               -- See Note [Deferring coercion errors to runtime]
-                               -- in TcSimplify
+-- An EvTerm is (usually) constructed by any of the constructors here
+-- and those more complicates ones who were moved to module TcEvTerm
 
-  | EvSuperClass EvTerm Int      -- n'th superclass. Used for both equalities and
-                                 -- dictionaries, even though the former have no
-                                 -- selector Id.  We count up from _0_
+-- | Any sort of evidence Id, including coercions
+evId ::  EvId -> EvExpr
+evId = Var
 
-  | EvLit EvLit       -- Dictionary for KnownNat and KnownSymbol classes.
-                      -- Note [KnownNat & KnownSymbol and EvLit]
+-- coercion bindings
+-- See Note [Coercion evidence terms]
+evCoercion :: TcCoercion -> EvExpr
+evCoercion = Coercion
 
-  | EvCallStack EvCallStack      -- Dictionary for CallStack implicit parameters
+-- | d |> co
+evCast :: EvExpr -> TcCoercion -> EvExpr
+evCast et tc | isReflCo tc = et
+             | otherwise   = Cast et tc
 
-  | EvTypeable Type EvTypeable   -- Dictionary for (Typeable ty)
+-- Dictionary instance application
+evDFunApp :: DFunId -> [Type] -> [EvExpr] -> EvExpr
+evDFunApp df tys ets = Var df `mkTyApps` tys `mkApps` ets
 
-  | EvSelector Id [Type] [EvTerm] -- Selector id plus the types at which it
-                                  -- should be instantiated, used for HasField
-                                  -- dictionaries; see Note [HasField instances]
-                                  -- in TcInterface
+-- Selector id plus the types at which it
+-- should be instantiated, used for HasField
+-- dictionaries; see Note [HasField instances]
+-- in TcInterface
+evSelector :: Id -> [Type] -> [EvExpr] -> EvExpr
+evSelector sel_id tys tms = Var sel_id `mkTyApps` tys `mkApps` tms
 
-  deriving Data.Data
 
+-- Dictionary for (Typeable ty)
+evTypeable :: Type -> EvTypeable -> EvTerm
+evTypeable = EvTypeable
 
 -- | Instructions on how to make a 'Typeable' dictionary.
 -- See Note [Typeable evidence terms]
 data EvTypeable
-  = EvTypeableTyCon [EvTerm]  -- ^ Dictionary for @Typeable (T k1..kn)@.
-                              -- The EvTerms are for the arguments
+  = EvTypeableTyCon TyCon [EvTerm]
+    -- ^ Dictionary for @Typeable T@ where @T@ is a type constructor with all of
+    -- its kind variables saturated. The @[EvTerm]@ is @Typeable@ evidence for
+    -- the applied kinds..
 
   | EvTypeableTyApp EvTerm EvTerm
     -- ^ Dictionary for @Typeable (s t)@,
-    -- given a dictionaries for @s@ and @t@
+    -- given a dictionaries for @s@ and @t@.
+
+  | EvTypeableTrFun EvTerm EvTerm
+    -- ^ Dictionary for @Typeable (s -> t)@,
+    -- given a dictionaries for @s@ and @t@.
 
   | EvTypeableTyLit EvTerm
     -- ^ Dictionary for a type literal,
     -- e.g. @Typeable "foo"@ or @Typeable 3@
     -- The 'EvTerm' is evidence of, e.g., @KnownNat 3@
     -- (see Trac #10348)
-
   deriving Data.Data
 
-data EvLit
-  = EvNum Integer
-  | EvStr FastString
-    deriving Data.Data
-
 -- | Evidence for @CallStack@ implicit parameters.
 data EvCallStack
   -- See Note [Overview of implicit CallStacks]
   = EvCsEmpty
-  | EvCsPushCall Name RealSrcSpan EvTerm
+  | EvCsPushCall Name RealSrcSpan EvExpr
     -- ^ @EvCsPushCall name loc stk@ represents a call to @name@, occurring at
     -- @loc@, in a calling context @stk@.
   deriving Data.Data
@@ -579,54 +612,6 @@ Conclusion: a new wanted coercion variable should be made mutable.
  from super classes will be "given" and hence rigid]
 
 
-Note [KnownNat & KnownSymbol and EvLit]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-A part of the type-level literals implementation are the classes
-"KnownNat" and "KnownSymbol", which provide a "smart" constructor for
-defining singleton values.  Here is the key stuff from GHC.TypeLits
-
-  class KnownNat (n :: Nat) where
-    natSing :: SNat n
-
-  newtype SNat (n :: Nat) = SNat Integer
-
-Conceptually, this class has infinitely many instances:
-
-  instance KnownNat 0       where natSing = SNat 0
-  instance KnownNat 1       where natSing = SNat 1
-  instance KnownNat 2       where natSing = SNat 2
-  ...
-
-In practice, we solve `KnownNat` predicates in the type-checker
-(see typecheck/TcInteract.hs) because we can't have infinitely many instances.
-The evidence (aka "dictionary") for `KnownNat` is of the form `EvLit (EvNum n)`.
-
-We make the following assumptions about dictionaries in GHC:
-  1. The "dictionary" for classes with a single method---like `KnownNat`---is
-     a newtype for the type of the method, so using a evidence amounts
-     to a coercion, and
-  2. Newtypes use the same representation as their definition types.
-
-So, the evidence for `KnownNat` is just a value of the representation type,
-wrapped in two newtype constructors: one to make it into a `SNat` value,
-and another to make it into a `KnownNat` dictionary.
-
-Also note that `natSing` and `SNat` are never actually exposed from the
-library---they are just an implementation detail.  Instead, users see
-a more convenient function, defined in terms of `natSing`:
-
-  natVal :: KnownNat n => proxy n -> Integer
-
-The reason we don't use this directly in the class is that it is simpler
-and more efficient to pass around an integer rather than an entier function,
-especially when the `KnowNat` evidence is packaged up in an existential.
-
-The story for kind `Symbol` is analogous:
-  * class KnownSymbol
-  * newtype SSymbol
-  * Evidence: EvLit (EvStr n)
-
-
 Note [Overview of implicit CallStacks]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 (See https://ghc.haskell.org/trac/ghc/wiki/ExplicitCallStack/ImplicitLocations)
@@ -751,17 +736,19 @@ Important Details:
 
 -}
 
-mkEvCast :: EvTerm -> TcCoercion -> EvTerm
+mkEvCast :: EvExpr -> TcCoercion -> EvExpr
 mkEvCast ev lco
   | ASSERT2(tcCoercionRole lco == Representational, (vcat [text "Coercion of wrong role passed to mkEvCast:", ppr ev, ppr lco]))
     isTcReflCo lco = ev
-  | otherwise      = EvCast ev lco
+  | otherwise      = evCast ev lco
 
-mkEvScSelectors :: EvTerm -> Class -> [TcType] -> [(TcPredType, EvTerm)]
+mkEvScSelectors :: EvExpr -> Class -> [TcType] -> [(TcPredType, EvExpr)]
 mkEvScSelectors ev cls tys
    = zipWith mk_pr (immSuperClasses cls tys) [0..]
   where
-    mk_pr pred i = (pred, EvSuperClass ev i)
+    mk_pr pred i = (pred, Var sc_sel_id `mkTyApps` tys `App` ev)
+      where
+        sc_sel_id  = classSCSelId cls i -- Zero-indexed
 
 emptyTcEvBinds :: TcEvBinds
 emptyTcEvBinds = EvBinds emptyBag
@@ -770,57 +757,71 @@ isEmptyTcEvBinds :: TcEvBinds -> Bool
 isEmptyTcEvBinds (EvBinds b)    = isEmptyBag b
 isEmptyTcEvBinds (TcEvBinds {}) = panic "isEmptyTcEvBinds"
 
-
 evTermCoercion :: EvTerm -> TcCoercion
 -- Applied only to EvTerms of type (s~t)
 -- See Note [Coercion evidence terms]
-evTermCoercion (EvId v)        = mkCoVarCo v
-evTermCoercion (EvCoercion co) = co
-evTermCoercion (EvCast tm co)  = mkCoCast (evTermCoercion tm) co
-evTermCoercion tm = pprPanic "evTermCoercion" (ppr tm)
+evTermCoercion (EvExpr (Var v))       = mkCoVarCo v
+evTermCoercion (EvExpr (Coercion co)) = co
+evTermCoercion (EvExpr (Cast tm co))  = mkCoCast (evTermCoercion (EvExpr tm)) co
+evTermCoercion tm                     = pprPanic "evTermCoercion" (ppr tm)
+
+
+{-
+************************************************************************
+*                                                                      *
+                  Free variables
+*                                                                      *
+************************************************************************
+-}
+
+findNeededEvVars :: EvBindMap -> VarSet -> VarSet
+findNeededEvVars ev_binds seeds
+  = transCloVarSet also_needs seeds
+  where
+   also_needs :: VarSet -> VarSet
+   also_needs needs = nonDetFoldUniqSet add emptyVarSet needs
+     -- It's OK to use nonDetFoldUFM here because we immediately
+     -- forget about the ordering by creating a set
+
+   add :: Var -> VarSet -> VarSet
+   add v needs
+     | Just ev_bind <- lookupEvBind ev_binds v
+     , EvBind { eb_is_given = is_given, eb_rhs = rhs } <- ev_bind
+     , is_given
+     = evVarsOfTerm rhs `unionVarSet` needs
+     | otherwise
+     = needs
 
 evVarsOfTerm :: EvTerm -> VarSet
-evVarsOfTerm (EvId v)             = unitVarSet v
-evVarsOfTerm (EvCoercion co)      = coVarsOfCo co
-evVarsOfTerm (EvDFunApp _ _ evs)  = mapUnionVarSet evVarsOfTerm evs
-evVarsOfTerm (EvSuperClass v _)   = evVarsOfTerm v
-evVarsOfTerm (EvCast tm co)       = evVarsOfTerm tm `unionVarSet` coVarsOfCo co
-evVarsOfTerm (EvDelayedError _ _) = emptyVarSet
-evVarsOfTerm (EvLit _)            = emptyVarSet
-evVarsOfTerm (EvCallStack cs)     = evVarsOfCallStack cs
-evVarsOfTerm (EvTypeable _ ev)    = evVarsOfTypeable ev
-evVarsOfTerm (EvSelector _ _ evs) = mapUnionVarSet evVarsOfTerm evs
+evVarsOfTerm (EvExpr e)         = exprSomeFreeVars isEvVar e
+evVarsOfTerm (EvTypeable _ ev)  = evVarsOfTypeable ev
 
 evVarsOfTerms :: [EvTerm] -> VarSet
 evVarsOfTerms = mapUnionVarSet evVarsOfTerm
 
+evVarsOfTypeable :: EvTypeable -> VarSet
+evVarsOfTypeable ev =
+  case ev of
+    EvTypeableTyCon _ e   -> mapUnionVarSet evVarsOfTerm e
+    EvTypeableTyApp e1 e2 -> evVarsOfTerms [e1,e2]
+    EvTypeableTrFun e1 e2 -> evVarsOfTerms [e1,e2]
+    EvTypeableTyLit e     -> evVarsOfTerm e
+
 -- | Do SCC analysis on a bag of 'EvBind's.
 sccEvBinds :: Bag EvBind -> [SCC EvBind]
 sccEvBinds bs = stronglyConnCompFromEdgedVerticesUniq edges
   where
-    edges :: [(EvBind, EvVar, [EvVar])]
+    edges :: [ Node EvVar EvBind ]
     edges = foldrBag ((:) . mk_node) [] bs
 
-    mk_node :: EvBind -> (EvBind, EvVar, [EvVar])
+    mk_node :: EvBind -> Node EvVar EvBind
     mk_node b@(EvBind { eb_lhs = var, eb_rhs = term })
-      = (b, var, nonDetEltsUFM (evVarsOfTerm term `unionVarSet`
+      = DigraphNode b var (nonDetEltsUniqSet (evVarsOfTerm term `unionVarSet`
                                 coVarsOfType (varType var)))
-      -- It's OK to use nonDetEltsUFM here as stronglyConnCompFromEdgedVertices
+      -- It's OK to use nonDetEltsUniqSet here as stronglyConnCompFromEdgedVertices
       -- is still deterministic even if the edges are in nondeterministic order
       -- as explained in Note [Deterministic SCC] in Digraph.
 
-evVarsOfCallStack :: EvCallStack -> VarSet
-evVarsOfCallStack cs = case cs of
-  EvCsEmpty -> emptyVarSet
-  EvCsPushCall _ _ tm -> evVarsOfTerm tm
-
-evVarsOfTypeable :: EvTypeable -> VarSet
-evVarsOfTypeable ev =
-  case ev of
-    EvTypeableTyCon es    -> evVarsOfTerms es
-    EvTypeableTyApp e1 e2 -> evVarsOfTerms [e1,e2]
-    EvTypeableTyLit e     -> evVarsOfTerm e
-
 {-
 ************************************************************************
 *                                                                      *
@@ -885,21 +886,8 @@ instance Outputable EvBind where
    -- We cheat a bit and pretend EqVars are CoVars for the purposes of pretty printing
 
 instance Outputable EvTerm where
-  ppr (EvId v)              = ppr v
-  ppr (EvCast v co)         = ppr v <+> (text "`cast`") <+> pprParendCo co
-  ppr (EvCoercion co)       = text "CO" <+> ppr co
-  ppr (EvSuperClass d n)    = text "sc" <> parens (ppr (d,n))
-  ppr (EvDFunApp df tys ts) = ppr df <+> sep [ char '@' <> ppr tys, ppr ts ]
-  ppr (EvLit l)             = ppr l
-  ppr (EvCallStack cs)      = ppr cs
-  ppr (EvDelayedError ty msg) =     text "error"
-                                <+> sep [ char '@' <> ppr ty, ppr msg ]
-  ppr (EvTypeable ty ev)      = ppr ev <+> dcolon <+> text "Typeable" <+> ppr ty
-  ppr (EvSelector sel tys ts) = ppr sel <+> sep [ char '@' <> ppr tys, ppr ts]
-
-instance Outputable EvLit where
-  ppr (EvNum n) = integer n
-  ppr (EvStr s) = text (show s)
+  ppr (EvExpr e)         = ppr e
+  ppr (EvTypeable ty ev) = ppr ev <+> dcolon <+> text "Typeable" <+> ppr ty
 
 instance Outputable EvCallStack where
   ppr EvCsEmpty
@@ -908,8 +896,9 @@ instance Outputable EvCallStack where
     = ppr (name,loc) <+> text ":" <+> ppr tm
 
 instance Outputable EvTypeable where
-  ppr (EvTypeableTyCon ts)    = text "TC" <+> ppr ts
+  ppr (EvTypeableTyCon ts _)  = text "TyCon" <+> ppr ts
   ppr (EvTypeableTyApp t1 t2) = parens (ppr t1 <+> ppr t2)
+  ppr (EvTypeableTrFun t1 t2) = parens (ppr t1 <+> arrow <+> ppr t2)
   ppr (EvTypeableTyLit t1)    = text "TyLit" <> ppr t1