One language that comes to mind is ReasonML. It doesn't have runtime checking. It's structural and compile time, but the guarantees are supposedly cast iron. https://reasonml-old.github.io/guide/language/type#design-de...

    type thing = 
      | String(string)
      | Bool(bool);

    let arr: list(thing) = [];

    let add = (item: thing, dst: list(thing)): list(thing) => {
      switch (item) {
      | String(s) => dst @ [String(s)] 
      | Bool(b) => dst @ [Bool(b)]    
      };
    };

    let newList = add(String("asd"), arr);

This doesn't work, since the dst array has to be one that can contain both string and bool in the first place.