Aby tohle fungovalo, musí být ta hodnota boxovaná (na-alokovaná na heapu a schovaná za, efektivně, pointer) a operace na ní se provádí přes dynamic dispatch (bude tam nějaký ekvivalent v-table), jinak by nebylo možné provést type erasure.
Teda, já jsem to vždycky chápal tak, že type erasure je způsob, jak typy odrbat. Kde by tam jako měla být schovaná vtable? A proč? Ve skutečnosti tam tu vtable potřebuješ v případě, kdy nechceš dělat type erasure...
Dobře, tak mějme ten příklad s maticí. Dejme tomu, že od nějaké velikosti Thr (jako threshold) používá implementace matice nějakou vymakanou reprezentaci v paměti kvůli ušetření místa pro velké matice. Ok? Teď dejme tomu, že máme operaci `col` na matici, která vrátí daný sloupec jako vektor. Tahle operace bude muset fungovat různě v závislosti na Thr, z úsporné reprezentace se čte sloupec jinak než z jednoduché.
Tak, a teď, ty napíšeš program, který načte matici ze souboru a bude chtít číst sloupce. Pokud by ta typová informace - v tomto případě velikost matice - byla komplet odstraněna, metoda `col` by neměla jak poznat, jak je konkrétní matice v paměti reprezentována, a tedy jak extrahovat sloupec. Proto bude muset ta matice si s sebou tu informaci vzít a držet si ji během runtime, buďto to může být nějaký tag, podle kterého udělá ta metoda `col` vidličku, anebo si s sebout vezme vtable, která bude u různých konkrétních hodnoty ukazovat na různé implementace `col`. Řešení s vtable je obecnější - těch typových parametrů může být více, chování se může v závislosti na nich více lišit.
V jazyce jako Rust nebo C++ tohle není potřeba, protože kompilátor zná dopředu všechny instanciace a provede monomofrizaci, ie. v podstatě z toho udělá různé typy s různými metodami, ale cena za to je, že není možné vytvořit tu hodnotu at runtime.
Není podstatné, že Lua je dynamický jazyk. Chtěl jsem tím uvést, že když jsem se kouknul do toho zdrojáku, tak tam žádné typové informace, které tvrdíš, že tam musí zůstat aby něco, nebyly.
Jak jsi poznal, že tam nebyly typové informace? V jazyce jako Lua má
každá hodnota runtime typovou informaci, tak fungují dynamicky typované jazyky, tzn. ty typy tam nemohly nebýt

---
Jinak podíval jsem se na C výstup Idris kompilátoru a je to prostě VM (verze idris je u mě 1.3.4). Toto je funkce alokující hodnotu, okopírováno z Idris runtime:
static inline Con * allocConF(VM * vm, uint32_t tag, uint16_t arity, int outer) { ... }
Hádejte, co je `tag`