隱式參數的順序如何影響idris？

Question

這種失敗：

> the ({A : Type} -> A -> {B : Type} -> B -> (A, B)) MkPair 
(input):1:5:When checking argument value to function Prelude.Basics.the: 
     Type mismatch between 
       A -> B1 -> (A, B1) (Type of MkPair) 
     and 
       A1 -> B -> (A1, B) (Expected type) 

     Specifically: 
       Type mismatch between 
         Pair A 
       and 
         \uv => uv -> uv 

這工作：

> ({A : Type} -> {B : Type} -> A -> B -> (A, B)) MkPair 
\A1, B1 => MkPair : A -> B -> (A, B) 

奇怪的是：

q : {A : Type} -> A -> {B : Type} -> B -> (A, B) 
q a b = MkPair a b 

> :t q 
q : A -> B -> (A, B) 

> :t MkPair 
MkPair : A -> B -> (A, B) 

爲什麼q和MkPair似乎有相同的類型？他們真的有相同的類型嗎？爲什麼隱式論證的順序很重要？

Answer 1

從某種意義上說，隱式參數與非隱式參數沒有區別。編譯器大多數時候會爲你推薦它們，但它們仍然是參數並且必須存在，因爲在覈心語言層面沒有隱含的參數。你可以問REPL顯示implicits你：

λΠ> :set showimplicits 
λΠ> :t MkPair 
Builtins.MkPair : {A : Type} -> {B : Type} -> (a : A) -> (b : B) -> (A, B) 
λΠ> :t q 
Main.q : {A : Type} -> A -> {B : Type} -> B -> (A, B) 

如果替換大括號普通括號中的上述類型，你會看到各類MkPair和q因爲不同的順序是不同的參數。