Что означает сообщение об ошибке «Несовершенство Вселенной» при работе с типами более высокого ранга?

Question

не Учитывая следующий код: Идрис

import Data.Vect 
import Data.Fin 

%default total 

fins : Vect n (Fin n) 
fins {n = Z} = [] 
fins {n = S n} = FZ :: map FS fins 

Permutation : Nat -> Type 
Permutation n = {a : Type} -> Vect n a -> Vect n a 

permutations : {n : Nat} -> Vect (fact n) (Permutation n) 
permutations {n = Z} = [id] 
permutations {n = S n} = 
    rewrite multCommutative (S n) (fact n) in 
    concat $ map inserts (permutations {n = n}) 
    where 
    inserts : Permutation k -> Vect (S k) (Permutation (S k)) 
    inserts pi = map (\i => \(x :: xs) => insertAt i x . pi $ xs) fins 

Я получаю следующее сообщение об ошибке от Идриса 0.9.16 (и никаких дополнительных подробностей):

Type checking .\Permutations.idr 
Permutations.idr:15:14:Universe inconsistency 

Однако, изменив его только чуть-чуть, так что второй раздел permutations становится

permutations {n = S n} = 
    rewrite multCommutative (S n) (fact n) in 
    concat . map inserts $ permutations {n = n} 

тогда он внезапно typechecks.

Есть ли какая-то особенная магия внутри Идриса, возможно, при обработке ($) и (.), similar to what GHC does, чтобы они работали в присутствии более высоких классов?

Answer 1

От Идриса 0.10.2, мой первоначальный код (с использованием concat $ map inserts (permutations {n = n}) в определении permutations) typechecks без икоты.