Remove ECast

The invariant that this used to ensure does not hold anymore, so
it was more confusing than not to have it.

src/Cryptol/Eval.hs

@@ -146,8 +146,6 @@ evalExpr env expr = case expr of
   EProofAbs _ e -> evalExpr env e
   EProofApp e   -> evalExpr env e
 
-  ECast e _ty -> evalExpr env e
-
   EWhere e ds -> {-# SCC "evalExpr->EWhere" #-} do
      env' <- evalDecls ds env
      evalExpr env' e

src/Cryptol/Eval/Reference.hs

@@ -188,7 +188,6 @@ evalExpr env expr =
     EAbs n _ty b   -> VFun (\v -> evalExpr (bindVar (n, v) env) b)
     EProofAbs _ e  -> evalExpr env e
     EProofApp e    -> evalExpr env e
-    ECast e _ty    -> evalExpr env e
     EWhere e dgs   -> evalExpr (foldl evalDeclGroup env dgs) e
 
 

src/Cryptol/Transform/MonoValues.hs

@@ -195,7 +195,6 @@ rewE rews = go
 
       EProofAbs x e   -> EProofAbs x <$> go e
 
-      ECast e t       -> ECast       <$> go e <*> return t
       EWhere e dgs    -> EWhere      <$> go e <*> inLocal
                                                   (mapM (rewDeclGroup rews) dgs)
 

src/Cryptol/Transform/Specialize.hs

@@ -99,8 +99,6 @@ specializeExpr expr =
     EAbs qn t e   -> EAbs qn t <$> specializeExpr e
     EProofAbs p e -> EProofAbs p <$> specializeExpr e
     EProofApp {}  -> specializeConst expr
-    ECast e t     -> ECast <$> specializeExpr e <*> pure t
-    -- TODO: if typeOf e == t, then drop the coercion.
     EWhere e dgs  -> specializeEWhere e dgs
 
 specializeMatch :: Match -> SpecM Match

src/Cryptol/TypeCheck/AST.hs

@@ -92,23 +92,6 @@ data Expr   = EList [Expr] Type         -- ^ List value (with type of elements)
 
             | EProofApp Expr {- proof -}
 
-            {- | if e : t1, then cast e : t2
-                 as long as we can prove that 't1 = t2'.
-                 We could express this in terms of a built-in constant.
-                 `cast :: {a,b} (a =*= b) => a -> b`
-
-                 Using the constant is a bit verbose though, because we
-                 end up with both the source and target type. So, instead
-                 we use this language construct, which only stores the
-                 target type, and the source type can be reconstructed
-                 from the expression.
-
-                 Another way to think of this is simply as an expression
-                 with an explicit type annotation.
-              -}
-            | ECast Expr Type
-
-
             | EWhere Expr [DeclGroup]
 
               deriving (Show, Generic, NFData)
@@ -220,9 +203,6 @@ instance PP (WithNames Expr) where
       ETApp e t     -> optParens (prec > 3)
                     $ ppWP 3 e <+> ppWP 4 t
 
-      ECast e t     -> optParens (prec > 0)
-                     ( ppWP 2 e <+> text ":" <+> ppW t )
-
       EWhere e ds   -> optParens (prec > 0)
                      ( ppW e $$ text "where"
                                      $$ nest 2 (vcat (map ppW ds))

src/Cryptol/TypeCheck/Infer.hs

@@ -108,7 +108,8 @@ appTys expr ts tGoal =
            ExtVar s   -> instantiateWith (EVar x) s ts
            CurSCC e t -> instantiateWith e (Forall [] [] t) ts
 
-         checkHasType e' t tGoal
+         checkHasType t tGoal
+         return e'
 
     P.ELit l -> do e <- desugarLiteral False l
                    appTys e ts tGoal
@@ -147,7 +148,8 @@ appTys expr ts tGoal =
                   (ie,t) <- instantiateWith e' (Forall [] [] tGoal) ts
                   -- XXX seems weird to need to do this, as t should be the same
                   -- as tGoal
-                  checkHasType ie t tGoal
+                  checkHasType t tGoal
+                  return ie
 
 
 inferTyParam :: P.TypeInst Name -> InferM (Located (Maybe Ident, Type))
@@ -186,7 +188,8 @@ checkE expr tGoal =
            ExtVar s   -> instantiateWith (EVar x) s []
            CurSCC e t -> return (e, t)
 
-         checkHasType e' t tGoal
+         checkHasType t tGoal
+         return e'
 
     P.ELit l -> (`checkE` tGoal) =<< desugarLiteral False l
 
@@ -308,7 +311,8 @@ checkE expr tGoal =
     P.ETyped e t ->
       do tSig <- checkTypeOfKind t KType
          e'   <- checkE e tSig
-         checkHasType e' tSig tGoal
+         checkHasType tSig tGoal
+         return e'
 
     P.ETypeVal t ->
       do l <- curRange
@@ -455,12 +459,12 @@ expectFun  = go []
                       newType (text "argument" <+> ordinal ix) KType
 
 
-checkHasType :: Expr -> Type -> Type -> InferM Expr
+checkHasType :: Type -> Type -> InferM ()
-checkHasType e inferredType givenType =
+checkHasType inferredType givenType =
   do ps <- unify givenType inferredType
      case ps of
-       [] -> return e
+       [] -> return ()
-       _  -> newGoals CtExactType ps >> return (ECast e givenType)
+       _  -> newGoals CtExactType ps
 
 
 checkFun :: Doc -> [P.Pattern Name] -> P.Expr Name -> Type -> InferM Expr

src/Cryptol/TypeCheck/Instantiate.hs

@@ -75,15 +75,11 @@ instantiateWithPos e (Forall as ps t) ts =
 The arguments that are provided will be instantiated as requested,
 the rest will be instantiated with fresh type variables.
 
-Note that we assume that type parameters are not normalized.
+EProofApp (ETApp e t)
-Generally, the resulting expression will look something like this:
-
-ECast (EProofApp (ETApp e t)) t1
 
   where
   - There will be one `ETApp t` for each insantiated type parameter;
   - there will be one `EProofApp` for each constraint on the schema;
-  - there will be `ECast` if we had equality constraints from normalization.
 -}
 instantiateWithNames :: Expr -> Schema -> [Located (Ident,Type)]
                      -> InferM (Expr,Type)

src/Cryptol/TypeCheck/Sanity.hs

@@ -318,12 +318,6 @@ exprSchema expr =
            (_,_)      -> reportError (BadProofTyVars as)
 
 
-    ECast e t ->
-      do checkTypeIs KType t
-         t1 <- exprType e
-         convertible t t1
-         return (tMono t)
-
     -- XXX: Check that defined things are disitnct?
     EWhere e dgs ->
       let go []       = exprSchema e

src/Cryptol/TypeCheck/Solver/Selector.hs

@@ -40,20 +40,20 @@ listType n =
      return (tSeq (tNum n) elems)
 
 
-improveSelector :: Selector -> Type -> InferM (Expr -> Expr)
+improveSelector :: Selector -> Type -> InferM ()
 improveSelector sel outerT =
   case sel of
     RecordSel _ mb -> cvt recordType mb
     TupleSel  _ mb -> cvt tupleType  mb
     ListSel   _ mb -> cvt listType   mb
   where
-  cvt _ Nothing   = return id
+  cvt _ Nothing   = return ()
   cvt f (Just a)  = do ty <- f a
                        cs <- unify ty outerT
                        case cs of
-                         [] -> return id
+                         [] -> return ()
                          _  -> do newGoals CtExactType cs
-                                  return (`ECast` ty)
+                                  return ()
 
 
 {- | Compute the type of a field based on the selector.
@@ -120,18 +120,17 @@ solveSelector sel outerT =
 tryHasGoal :: HasGoal -> InferM ()
 tryHasGoal has
   | TCon (PC (PHas sel)) [ th, ft ] <- goal (hasGoal has) =
-    do outerCast <- improveSelector sel th
+    do improveSelector sel th
        outerT    <- tNoUser `fmap` applySubst th
        mbInnerT  <- solveSelector sel outerT
        case mbInnerT of
          Nothing -> addHasGoal has
          Just innerT ->
            do cs <- unify innerT ft
-              innerCast <- case cs of
+              case cs of
-                             [] -> return id
+                [] -> return ()
-                             _  -> do newGoals CtExactType cs
+                _  -> newGoals CtExactType cs
-                                      return (`ECast` ft)
+              solveHasGoal (hasName has) (`ESel` sel)
-              solveHasGoal (hasName has) (innerCast . (`ESel` sel) . outerCast)
 
   | otherwise = panic "hasGoalSolved"
                   [ "Unexpected selector proposition:"

src/Cryptol/TypeCheck/Subst.hs

@@ -255,7 +255,6 @@ instance TVars Expr where
         ETApp e t     -> ETApp (go e) (apSubst su t)
         EProofAbs p e -> EProofAbs (apSubst su p) (go e)
         EProofApp e   -> EProofApp (go e)
-        ECast e t     -> ECast (go e) (apSubst su t)
 
         EVar {}       -> expr
 

src/Cryptol/TypeCheck/TypeOf.hs

@@ -40,7 +40,6 @@ fastTypeOf tyenv expr =
                         Just (_, t) -> t
                         Nothing     -> panic "Cryptol.TypeCheck.TypeOf.fastTypeOf"
                                          [ "EApp with non-function operator" ]
-    ECast _ t     -> t
     -- Polymorphic fragment
     EVar      {}  -> polymorphic
     ETAbs     {}  -> polymorphic
@@ -93,7 +92,6 @@ fastSchemaOf tyenv expr =
     EComp  {}      -> monomorphic
     EApp   {}      -> monomorphic
     EAbs   {}      -> monomorphic
-    ECast  {}      -> monomorphic
   where
     monomorphic = Forall [] [] (fastTypeOf tyenv expr)