Typy zależne

Czytam o Idrisie i typach zależnych, np.

data Fin : Nat -> Type 
FZ : Fin (S k)
FS : Fin k -> Fin (S k)

O ile rozumiem ideę, to taki konstrukt reprezentuje zbiór skończony. I teraz kilka wątpliwości:

1. Fin 2 zwraca typ, który ma 2 konstruktory: FZ oraz FS?

2. Fin 2 dopuszcza dwie wartości: FZ oraz FS FZ. Z sygnatury FS wynika, że skoro FS FZ jest wartością Fin 2, tzn. że FZ musi być typu Fin 1, a może nie musi?

3. Jeśli rozważę Fin 3, to ten typ dopuszcza 3 wartości: FZ, FS FZ oraz FS FS FZ. Skoro FS FS FZ jest Fin 3, to FS FZ jest Fin 2, ale wówczas nie kłóci się to z tym, że ma być typu Fin 3?

4. Jeśli sie nie kłóci, tzn. że takie np. FS FZ jest typu Fin k dla każdego k>1 i wówczas wartość może pasowac do wielu typów? Jeśli tak, to czy to powód ograniczonego type inference w Idrisie?

Ad . 4. Ja idrisa nie znam w ogóle ale jak patrzę na kod źródłowy to myślę że wartość nie może pasować do wielu typów. To tak jak masz wartość 1. W Haskellu to będzie domyślnie Int czyli liczba ze znakiem i tyle bitów ile ma procesor, oczywiście możesz mieć też wartości 1::Int64 1::Int32 1::Word (int bez znaku), ale to sa różne wartości) i w wielu pewnie będzie potrzebna konwersja

I teraz możesz sobie wywołać natToFin 1 2 i natToFin 1 3 i będą to różne wartości bo będą różnych typów i na oko nie wstawisz jednej w miejsce drugiej. Trzeba by zrobić konwersje

powiedziałbym że jedyna różnica to że w normalnym języku masz typy Int16, Int32, Int64 a w Idrisie masz typy Fin 1, Fin 2, Fin 3, Fin 4 itd