Heapster: Rust typechecking fails with new entree translation

[m-yac]

As of #1778 many of the rust examples in heapster-saw/examples fail to typecheck, and so are currently commented-out in the respective files. Most fail with a similar-looking error, having something to do with Prelude.composeS. For example, from xor_swap_rust.saw:

While typechecking term: 
  let { x@1 = Prelude.Vec 64 Prelude.Bool
    }
 in Prelude.composeS Prelude.VoidEv Prelude.emptyFunStack
      #(-empty-)
      x@1
      x@1
      (\(x_local0 : #(-empty-)) ->
         let { x@2 = Prelude.Vec 64 Prelude.Bool
             }
          in Prelude.retS Prelude.VoidEv
               (Prelude.pushFunStack
                  (Prelude.Cons1
                     Prelude.LetRecType
                     (Prelude.LRT_Fun
                        x@2
                        (\(perm0 : x@2) ->
                           let { x@3 = Prelude.Vec 64 Prelude.Bool
                               }
                            in Prelude.LRT_Fun
                                 x@3
                                 (\(perm1 : x@3) ->
                                    let { x@4 = (ps : #(-empty-))
                                          -> Prelude.SpecM Prelude.VoidEv Prelude.emptyFunStack
                                               (Prelude.Vec 64 Prelude.Bool)
                                        }
                                     in Prelude.LRT_Ret (x@4 * x@4))))
                     (Prelude.Nil1 Prelude.LetRecType))
                  Prelude.emptyFunStack)
               x@2
               z10)
Inferred type
  (x_local0 : #(-empty-))
-> let { x@1 = Prelude.Vec 64 Prelude.Bool
    }
 in Prelude.SpecM Prelude.VoidEv
      (Prelude.pushFunStack
         (Prelude.Cons1
            Prelude.LetRecType
            (Prelude.LRT_Fun
               x@1
               (\(perm0 : x@1) ->
                  let { x@2 = Prelude.Vec 64 Prelude.Bool
                      }
                   in Prelude.LRT_Fun
                        x@2
                        (\(perm1 : x@2) ->
                           let { x@3 = (ps : #(-empty-))
                                 -> Prelude.SpecM Prelude.VoidEv Prelude.emptyFunStack
                                      (Prelude.Vec 64 Prelude.Bool)
                               }
                            in Prelude.LRT_Ret (x@3 * x@3))))
            (Prelude.Nil1 Prelude.LetRecType))
         Prelude.emptyFunStack)
      x@1
Not a subtype of expected type
  #(-empty-)
-> Prelude.SpecM Prelude.VoidEv Prelude.emptyFunStack
     (Prelude.Vec 64 Prelude.Bool)
For term
  \(x_local0 : #(-empty-)) ->
  let { x@1 = Prelude.Vec 64 Prelude.Bool
      }
   in Prelude.retS Prelude.VoidEv
        (Prelude.pushFunStack
           (Prelude.Cons1
              Prelude.LetRecType
              (Prelude.LRT_Fun
                 x@1
                 (\(perm0 : x@1) ->
                    let { x@2 = Prelude.Vec 64 Prelude.Bool
                        }
                     in Prelude.LRT_Fun
                          x@2
                          (\(perm1 : x@2) ->
                             let { x@3 = (ps : #(-empty-))
                                   -> Prelude.SpecM Prelude.VoidEv Prelude.emptyFunStack
                                        (Prelude.Vec 64 Prelude.Bool)
                                 }
                              in Prelude.LRT_Ret (x@3 * x@3))))
              (Prelude.Nil1 Prelude.LetRecType))
           Prelude.emptyFunStack)
        x@1
        z10