-
Notifications
You must be signed in to change notification settings - Fork 0
/
InferenceInAgda.html
1767 lines (1707 loc) · 423 KB
/
InferenceInAgda.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<meta http-equiv="Content-Style-Type" content="text/css" />
<meta name="generator" content="pandoc" />
<title></title>
<style type="text/css">code{white-space: pre;}</style>
</head>
<body>
<div id="TOC">
<ul>
<li><a href="#inference-in-agda">Inference in Agda</a><ul>
<li><a href="#preface">Preface</a></li>
<li><a href="#intro">Intro</a></li>
<li><a href="#imports">Imports</a></li>
<li><a href="#basics-of-type-inference">Basics of type inference</a></li>
<li><a href="#let-where-mutual"><code>let</code>, <code>where</code>, <code>mutual</code></a></li>
<li><a href="#unification-intro">Unification intro</a></li>
<li><a href="#inference-and-pattern-matching">Inference and pattern matching</a></li>
<li><a href="#inference-and-constructors">Inference and constructors</a></li>
<li><a href="#implicit-arguments">Implicit arguments</a></li>
<li><a href="#an-underspecified-argument-example">An underspecified argument example</a></li>
<li><a href="#not-dependent-enough">Not dependent enough</a></li>
<li><a href="#inferring-implicits">Inferring implicits</a></li>
<li><a href="#arguments-of-data-types">Arguments of data types</a><ul>
<li><a href="#comparison-to-haskell">Comparison to Haskell</a></li>
<li><a href="#under-the-hood">Under the hood</a></li>
</ul></li>
<li><a href="#nicer-notation">Nicer notation</a></li>
<li><a href="#type-functions">Type functions</a><ul>
<li><a href="#comparison-to-haskell-1">Comparison to Haskell</a></li>
</ul></li>
<li><a href="#data-constructors">Data constructors</a></li>
<li><a href="#reduction">Reduction</a></li>
<li><a href="#pattern-matching">Pattern matching</a><ul>
<li><a href="#a-constant-argument">A constant argument</a></li>
<li><a href="#a-non-constant-argument">A non-constant argument</a></li>
<li><a href="#examples">Examples</a></li>
<li><a href="#generalization">Generalization</a></li>
<li><a href="#constructor-headed-functions"><a href="https://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.FindingTheValuesOfImplicitArguments">Constructor-headed functions</a></a></li>
<li><a href="#constructorargument-headed-functions">Constructor/argument-headed functions</a></li>
</ul></li>
<li><a href="#eta-rules">Eta-rules</a><ul>
<li><a href="#computing-predicates-division">Computing predicates: division</a></li>
<li><a href="#bonus-singletons">Bonus: singletons</a></li>
<li><a href="#generating-type-level-data">Generating type-level data</a></li>
</ul></li>
<li><a href="#universe-levels">Universe levels</a></li>
<li><a href="#epilogue">Epilogue</a></li>
<li><a href="#acknowledgements">Acknowledgements</a></li>
</ul></li>
</ul>
</div>
<pre><style type="text/css">
<!--
body {
color: #000000;
background-color: #ffffff;
}
.agda2-highlight-bound-variable {
}
.agda2-highlight-catchall-clause {
/* agda2-highlight-catchall-clause-face */
background-color: #f5f5f5;
}
.agda2-highlight-coverage-problem {
/* agda2-highlight-coverage-problem-face */
background-color: #f5deb3;
}
.agda2-highlight-datatype {
/* agda2-highlight-datatype-face */
color: #0000cd;
}
.agda2-highlight-field {
/* agda2-highlight-field-face */
color: #ee1289;
}
.agda2-highlight-function {
/* agda2-highlight-function-face */
color: #0000cd;
}
.agda2-highlight-inductive-constructor {
/* agda2-highlight-inductive-constructor-face */
color: #008b00;
}
.agda2-highlight-keyword {
/* agda2-highlight-keyword-face */
color: #cd6600;
}
.agda2-highlight-module {
/* agda2-highlight-module-face */
color: #a020f0;
}
.agda2-highlight-number {
/* agda2-highlight-number-face */
color: #a020f0;
}
.agda2-highlight-operator {
}
.agda2-highlight-postulate {
/* agda2-highlight-postulate-face */
color: #0000cd;
}
.agda2-highlight-primitive {
/* agda2-highlight-primitive-face */
color: #0000cd;
}
.agda2-highlight-primitive-type {
/* agda2-highlight-primitive-type-face */
color: #0000cd;
}
.agda2-highlight-record {
/* agda2-highlight-record-face */
color: #0000cd;
}
.agda2-highlight-symbol {
/* agda2-highlight-symbol-face */
color: #404040;
}
.agda2-highlight-unsolved-constraint {
/* agda2-highlight-unsolved-constraint-face */
background-color: #ffff00;
}
.agda2-highlight-unsolved-meta {
/* agda2-highlight-unsolved-meta-face */
background-color: #ffff00;
}
.comment {
/* font-lock-comment-face */
color: #b22222;
}
.comment-delimiter {
/* font-lock-comment-delimiter-face */
color: #b22222;
}
.default {
/* default */
color: #000000;
background-color: #ffffff;
}
code {
white-space: pre;
background-color: #f0f0f0;
display: inline-block
}
blockquote {
padding: 0 1em;
color: #6a737d;
border-left: 0.25em solid #d1d5da;
}
a:hover {
text-decoration: underline;
}
-->
</style></pre>
<h1 id="inference-in-agda">Inference in Agda</h1>
<pre><span class="agda2-highlight-keyword">module</span> <span class="agda2-highlight-module">InferenceInAgda</span> <span class="agda2-highlight-keyword">where</span>
</pre>
<p>This is a tutorial on how Agda infers things.</p>
<p>For sources, issue reports or contributing go to <a href="https://github.com/effectfully/inference-in-agda">the GitHub page</a>.</p>
<h2 id="preface">Preface</h2>
<p>Agda is a wonderful language and its unification engines are exemplary, practical, improve over time and work predictably well. Unification engines are one notable distiction between Agda and other dependently typed languages (such as Idris 1, Coq, Lean, etc). I'm saying "unification engines", because there are two of them:</p>
<ul>
<li>unification used for getting convenient and powerful pattern matching</li>
<li>unification used for inferring values of implicit arguments</li>
</ul>
<p>These are two completely distinct machineries. This tutorial covers only the latter for the moment being as it's what gives Agda its inference capabilities. I'll probably say a few words about the former once I forget how hard it is to write long technical texts.</p>
<p>This tutorial primarily targets</p>
<ul>
<li>users of Agda who want to understand how to write code to make more things inferrable</li>
<li>a general audience curious about dependent types and what can be done with them</li>
<li>people implementing powerful dependently typed languages and looking for features to support (most of what is described here are tricks that I use in may day-to-day work (when it involves Agda) and I'd definitely want to see them available in languages that are yet to come)</li>
</ul>
<p>Higher-order unification is not covered. It's a highly advanced topic and from the user's perspective diving into higher-order unification has a rather big cost/benefit ratio: I don't remember tweaking my code to fit it into the pattern fragment or doing anything else of this kind to help Agda unify things in the higher-order case. Agda would barely be usable without the built-in higher-order unification, but it's mostly invisible to the user and just works.</p>
<p>Analogously, no attempt to dissect Agda's internals is performed. Agda is well-designed enough not to force the user to worry about the peculiarities of the implementation (like when something gets postponed or in what order equations get solved). If you do want to learn about the internals, I recommend reading <a href="https://www.researchgate.net/publication/228571999_Type_checking_in_the_presence_of_meta-variables">Type checking in the presence of meta-variables</a> and <a href="http://www.cse.chalmers.se/~abela/unif-sigma-long.pdf">Higher-Order Dynamic Pattern Unification for Dependent Types and Records</a>.</p>
<p>And if you want to learn about internals of unification powering the pattern matching engine, then it's all elaborated in detail by Jesper Cockx in his <a href="https://jesper.sikanda.be/files/thesis-final-digital.pdf">PhD thesis</a>. Section "3.6 Related work" of it shortly describes differences between the requirements for the two kinds of unification.</p>
<h2 id="intro">Intro</h2>
<p>Agda only infers values that are uniquely determined by the current context. I.e. Agda doesn't try to guess: it either fails to infer a value or infers the definitive one. Even though this makes the unification algorithm weaker than it could be, it also makes it reliable and predictable. Whenever Agda infers something, you can be sure that this is the thing that you wanted and not just a random guess that would be different if you provided more information to the type checker (but Agda does have a guessing machinery called <a href="https://agda.readthedocs.io/en/v2.6.0.1/tools/auto.html">Agsy</a> that can be used interactively, so that no guessing needs to be done by the type checker and everything inferred is visible to the user).</p>
<p>We'll look into basics of type inference in Agda and then move to more advanced patterns. But first, some imports:</p>
<h2 id="imports">Imports</h2>
<pre><span class="agda2-highlight-keyword">open</span> <span class="agda2-highlight-keyword">import</span> <span class="agda2-highlight-module">Level</span> <span class="agda2-highlight-keyword">renaming</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-primitive">suc</span> <span class="agda2-highlight-symbol">to</span> <span class="agda2-highlight-primitive">lsuc</span><span class="agda2-highlight-symbol">;</span> <span class="agda2-highlight-primitive">zero</span> <span class="agda2-highlight-symbol">to</span> <span class="agda2-highlight-primitive">lzero</span><span class="agda2-highlight-symbol">)</span>
<span class="agda2-highlight-keyword">open</span> <span class="agda2-highlight-keyword">import</span> <span class="agda2-highlight-module">Function</span> <span class="agda2-highlight-keyword">using</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-operator"><span class="agda2-highlight-function">_$_</span></span><span class="agda2-highlight-symbol">;</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-function">_$′_</span></span><span class="agda2-highlight-symbol">;</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-function">_∘_</span></span><span class="agda2-highlight-symbol">;</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-function">_∘′_</span></span><span class="agda2-highlight-symbol">;</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-function">_∋_</span></span><span class="agda2-highlight-symbol">;</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-function">case_of_</span></span><span class="agda2-highlight-symbol">)</span> <span class="agda2-highlight-keyword">renaming</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-operator"><span class="agda2-highlight-function">_|>_</span></span> <span class="agda2-highlight-symbol">to</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-function">_&_</span></span><span class="agda2-highlight-symbol">;</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-function">_|>′_</span></span> <span class="agda2-highlight-symbol">to</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-function">_&′_</span></span><span class="agda2-highlight-symbol">)</span>
<span class="agda2-highlight-keyword">open</span> <span class="agda2-highlight-keyword">import</span> <span class="agda2-highlight-module">Relation.Binary.PropositionalEquality</span>
<span class="agda2-highlight-keyword">open</span> <span class="agda2-highlight-keyword">import</span> <span class="agda2-highlight-module">Data.Empty</span> <span class="agda2-highlight-keyword">using</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-datatype">⊥</span><span class="agda2-highlight-symbol">)</span>
<span class="agda2-highlight-keyword">open</span> <span class="agda2-highlight-keyword">import</span> <span class="agda2-highlight-module">Data.Unit.Base</span> <span class="agda2-highlight-keyword">using</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-record">⊤</span><span class="agda2-highlight-symbol">;</span> <span class="agda2-highlight-inductive-constructor">tt</span><span class="agda2-highlight-symbol">)</span>
<span class="agda2-highlight-keyword">open</span> <span class="agda2-highlight-keyword">import</span> <span class="agda2-highlight-module">Data.Bool.Base</span> <span class="agda2-highlight-keyword">using</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-datatype">Bool</span><span class="agda2-highlight-symbol">;</span> <span class="agda2-highlight-inductive-constructor">true</span><span class="agda2-highlight-symbol">;</span> <span class="agda2-highlight-inductive-constructor">false</span><span class="agda2-highlight-symbol">;</span> <span class="agda2-highlight-function">not</span><span class="agda2-highlight-symbol">)</span> <span class="agda2-highlight-keyword">renaming</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-operator"><span class="agda2-highlight-function">_∨_</span></span> <span class="agda2-highlight-symbol">to</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-function">_||_</span></span><span class="agda2-highlight-symbol">;</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-function">_∧_</span></span> <span class="agda2-highlight-symbol">to</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-function">_&&_</span></span><span class="agda2-highlight-symbol">)</span>
<span class="agda2-highlight-keyword">open</span> <span class="agda2-highlight-keyword">import</span> <span class="agda2-highlight-module">Data.Nat.Base</span> <span class="agda2-highlight-keyword">using</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-datatype">ℕ</span><span class="agda2-highlight-symbol">;</span> <span class="agda2-highlight-inductive-constructor">zero</span><span class="agda2-highlight-symbol">;</span> <span class="agda2-highlight-inductive-constructor">suc</span><span class="agda2-highlight-symbol">;</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-primitive">_+_</span></span><span class="agda2-highlight-symbol">;</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-primitive">_*_</span></span><span class="agda2-highlight-symbol">;</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-primitive">_∸_</span></span><span class="agda2-highlight-symbol">)</span>
<span class="agda2-highlight-keyword">open</span> <span class="agda2-highlight-keyword">import</span> <span class="agda2-highlight-module">Data.Product</span> <span class="agda2-highlight-keyword">using</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-operator"><span class="agda2-highlight-function">_×_</span></span><span class="agda2-highlight-symbol">;</span> <span class="agda2-highlight-record">Σ</span><span class="agda2-highlight-symbol">;</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-inductive-constructor">_,_</span></span><span class="agda2-highlight-symbol">;</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-function">_,′_</span></span><span class="agda2-highlight-symbol">)</span>
</pre>
<h2 id="basics-of-type-inference">Basics of type inference</h2>
<pre><span class="agda2-highlight-keyword">module</span> <span class="agda2-highlight-module">BasicsOfTypeInference</span> <span class="agda2-highlight-keyword">where</span>
</pre>
<p>Some preliminaries: the type of lists is defined as (ignoring universe polymorphism)</p>
<pre> <span class="agda2-highlight-keyword">infixr</span> <span class="agda2-highlight-number">5</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-inductive-constructor">_∷_</span></span>
<span class="agda2-highlight-keyword">data</span> <span class="agda2-highlight-datatype">List</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-primitive-type">Set</span><span class="agda2-highlight-symbol">)</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-primitive-type">Set</span> <span class="agda2-highlight-keyword">where</span>
<span class="agda2-highlight-inductive-constructor">[]</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-datatype">List</span> <span class="agda2-highlight-bound-variable">A</span>
<span class="agda2-highlight-operator"><span class="agda2-highlight-inductive-constructor">_∷_</span></span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-datatype">List</span> <span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-datatype">List</span> <span class="agda2-highlight-bound-variable">A</span>
</pre>
<p>Agda sees <code>[]</code> as having the following type: <code>∀ {A} -> List A</code>, however if you ask Agda what the type of <code>[]</code> is (by creating a hole in this module via <code>_ = ?</code>, putting there <code>[]</code> and typing <code>C-c C-d</code>. Or you can open the current module via <code>open BasicsOfTypeInference</code> and type <code>C-c C-d []</code> without introducing a hole), you'll get something like</p>
<pre><code> List _A_42</code></pre>
<p>(where <code>42</code> is some arbitrary number that Agda uses to distinguish between variables that have identical textual names, but are bound in distinct places)</p>
<p>That <code>_A_42</code> is a metavariable and Agda expects it to be resolved in the current context. If the context does not provide enough information for resolution to happen, Agda just reports that the metavariable is not resolved, i.e. Agda doesn't accept the code.</p>
<p>In contrast, Haskell is perfectly fine with <code>[]</code> and infers its type as <code>forall a. [a]</code>.</p>
<p>So Agda and Haskell think of <code>[]</code> having the same type</p>
<pre><code> ∀ {A} -> List A -- in Agda
forall a. [a] -- in Haskell</code></pre>
<p>but Haskell infers this type on the top level unlike Agda which expects <code>A</code> to be either resolved or explicitly bound.</p>
<p>You can make Agda infer the same type that Haskell infers by explicitly binding a type variable via a lambda:</p>
<pre> <span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-symbol">λ</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">A</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-inductive-constructor">[]</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">A</span><span class="agda2-highlight-symbol">}</span>
</pre>
<p>(<code>_ = <...></code> is an anonymous definition: we ask Agda to type check something, but don't bother giving it a name, because we're not going to use it later)</p>
<p>This definition is accepted, which means that Agda has inferred its type successfully.</p>
<p>Note that</p>
<pre><code> _ {A} = [] {A}</code></pre>
<p>means the same thing as the previous expression, but doesn't type check. It's just a syntactic limitation: certain things are allowed in patterns but not in lambdas and vice versa.</p>
<p>Agda can infer monomorphic types directly without any hints:</p>
<pre> <span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-inductive-constructor">true</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-inductive-constructor">∷</span></span> <span class="agda2-highlight-inductive-constructor">[]</span>
</pre>
<p>Type inference works not only with lambdas binding implicit arguments, but also explicit ones. And types of latter arguments can depend on earlier arguments. E.g.</p>
<pre> <span class="agda2-highlight-function">id₁</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-symbol">λ</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-primitive-type">Set</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-bound-variable">x</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-bound-variable">A</span><span class="agda2-highlight-symbol">)</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">x</span>
</pre>
<p>is the regular <code>id</code> function spelled as</p>
<pre><code> id :: forall a. a -> a
id x = x</code></pre>
<p>in Haskell.</p>
<p>Partially or fully applied <code>id₁</code> doesn't need a type signature either:</p>
<pre> <span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-function">id₁</span>
<span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-function">id₁</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-datatype">Bool</span><span class="agda2-highlight-symbol">}</span>
<span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-function">id₁</span> <span class="agda2-highlight-inductive-constructor">true</span>
</pre>
<p>You can even interleave implicit and explicit arguments and partial applications (and so full ones as well) will still be inferrable:</p>
<pre> <span class="agda2-highlight-function">const</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-symbol">λ</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-primitive-type">Set</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-bound-variable">x</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-bound-variable">A</span><span class="agda2-highlight-symbol">)</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">B</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-primitive-type">Set</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-bound-variable">y</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-bound-variable">B</span><span class="agda2-highlight-symbol">)</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">x</span>
<span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-function">const</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-datatype">Bool</span><span class="agda2-highlight-symbol">}</span>
<span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-function">const</span> <span class="agda2-highlight-inductive-constructor">true</span>
</pre>
<p>Finally, you don't need to specify a type signature for an alias, even if that alias has a different fixity than what it's defined in terms of. My favourite example is this:</p>
<pre> <span class="agda2-highlight-operator"><span class="agda2-highlight-function">_∘</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-function">_∘_</span></span>
</pre>
<p>It's an operator that allows us to compose a function with an n-ary function. In Haskell we have libraries like <a href="https://hackage.haskell.org/package/composition">composition</a> that define a bunch of n-ary composition operators like</p>
<pre><code> (.*) :: (c -> d) -> (a -> b -> c) -> a -> b -> d
(.**) :: (d -> e) -> (a -> b -> c -> d) -> a -> b -> c -> e
etc</code></pre>
<p>but in Agda we can get away with a single additional postfix operator and construct all of the above on the fly. For example:</p>
<pre> <span class="comment">-- Composing `suc` with 2-ary `_+_`</span>
<span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-inductive-constructor">suc</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-function">∘</span></span> <span class="agda2-highlight-operator"><span class="agda2-highlight-function">∘</span></span> <span class="agda2-highlight-operator"><span class="agda2-highlight-primitive">_+_</span></span>
<span class="comment">-- Composing `suc` with a random 3-ary function.</span>
<span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-inductive-constructor">suc</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-function">∘</span></span> <span class="agda2-highlight-operator"><span class="agda2-highlight-function">∘</span></span> <span class="agda2-highlight-operator"><span class="agda2-highlight-function">∘</span></span> <span class="agda2-highlight-function">f</span> <span class="agda2-highlight-keyword">where</span>
<span class="agda2-highlight-function">f</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-symbol">λ</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-bound-variable">x</span> <span class="agda2-highlight-bound-variable">y</span> <span class="agda2-highlight-bound-variable">z</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-datatype">ℕ</span><span class="agda2-highlight-symbol">)</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-number">0</span>
</pre>
<p>Note that <code>_∘</code> and <code>_∘_</code> are two different operators (in particular, the former is postfix and the latter is infix) that happen to be called the same. We could have called <code>_∘</code> differently of course, but since Agda is able to distinguish between the two based on how they're used (there's no <code>∘_</code> and so Agda knows that the only way to parse <code>suc ∘ ∘ ∘ f</code> is <code>((suc ∘) ∘) ∘ f</code>, which is exactly what one'd write in Haskell), it's just nice to make the two operators share the name.</p>
<h2 id="let-where-mutual"><code>let</code>, <code>where</code>, <code>mutual</code></h2>
<pre><span class="agda2-highlight-keyword">module</span> <span class="agda2-highlight-module">LetWhereMutual</span> <span class="agda2-highlight-keyword">where</span>
</pre>
<p>In Agda bindings that are not marked with <code>abstract</code> are transparent, i.e. writing, say, <code>let v = e in b</code> is the same thing as directly substituting <code>e</code> for <code>v</code> in <code>b</code> (<code>[e/v]b</code>). For example all of these type check:</p>
<pre> <span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-datatype">Bool</span>
<span class="agda2-highlight-symbol">_</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-keyword">let</span> <span class="agda2-highlight-bound-variable">𝔹</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-datatype">Bool</span>
<span class="agda2-highlight-bound-variable">t</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-bound-variable">𝔹</span>
<span class="agda2-highlight-bound-variable">t</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-inductive-constructor">true</span>
<span class="agda2-highlight-keyword">in</span> <span class="agda2-highlight-bound-variable">t</span>
<span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-datatype">Bool</span>
<span class="agda2-highlight-symbol">_</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-function">t</span> <span class="agda2-highlight-keyword">where</span>
<span class="agda2-highlight-function">𝔹</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-datatype">Bool</span>
<span class="agda2-highlight-function">t</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-function">𝔹</span>
<span class="agda2-highlight-function">t</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-inductive-constructor">true</span>
<span class="agda2-highlight-function">𝔹</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-datatype">Bool</span>
<span class="agda2-highlight-function">t</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-function">𝔹</span>
<span class="agda2-highlight-function">t</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-inductive-constructor">true</span>
<span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-datatype">Bool</span>
<span class="agda2-highlight-symbol">_</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-function">t</span>
</pre>
<p>Unlike Haskell Agda does not have <a href="https://www.haskell.org/ghc/blog/20100930-LetGeneralisationInGhc7.html">let-generalization</a>, i.e. this valid Haskell code:</p>
<pre><code> p :: (Bool, Integer)
p = let i x = x in (i True, i 1)</code></pre>
<p>has to be written either with an explicit type signature for <code>i</code>:</p>
<pre> <span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-datatype">Bool</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-function">×</span></span> <span class="agda2-highlight-datatype">ℕ</span>
<span class="agda2-highlight-symbol">_</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-keyword">let</span> <span class="agda2-highlight-bound-variable">i</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-primitive-type">Set</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">A</span>
<span class="agda2-highlight-bound-variable">i</span> <span class="agda2-highlight-bound-variable">x</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-bound-variable">x</span>
<span class="agda2-highlight-keyword">in</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-bound-variable">i</span> <span class="agda2-highlight-inductive-constructor">true</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-inductive-constructor">,</span></span> <span class="agda2-highlight-bound-variable">i</span> <span class="agda2-highlight-number">1</span><span class="agda2-highlight-symbol">)</span>
</pre>
<p>or in an equivalent way like</p>
<pre> <span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-datatype">Bool</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-function">×</span></span> <span class="agda2-highlight-datatype">ℕ</span>
<span class="agda2-highlight-symbol">_</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-keyword">let</span> <span class="agda2-highlight-bound-variable">i</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-symbol">λ</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">A</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-bound-variable">x</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-bound-variable">A</span><span class="agda2-highlight-symbol">)</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">x</span>
<span class="agda2-highlight-keyword">in</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-bound-variable">i</span> <span class="agda2-highlight-inductive-constructor">true</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-inductive-constructor">,</span></span> <span class="agda2-highlight-bound-variable">i</span> <span class="agda2-highlight-number">1</span><span class="agda2-highlight-symbol">)</span>
</pre>
<p>So Agda infers polymorphic types neither on the top level nor locally.</p>
<p>In Haskell types of bindings can be inferred from how those bindings are used later. E.g. the inferred type of a standalone</p>
<pre><code> one = 1</code></pre>
<p>is <code>Integer</code> (see <a href="https://wiki.haskell.org/Monomorphism_restriction">monomorphism restriction</a>), but in</p>
<pre><code> one = 1
one' = one :: Word</code></pre>
<p>the inferred type of <code>one</code> is <code>Word</code> rather than <code>Integer</code>.</p>
<p>This is not the case in Agda, e.g. a type for</p>
<pre><code> i = λ x -> x</code></pre>
<p>is not going to be inferred regardless of how this definition is used later. However if you use <code>let</code>, <code>where</code> or <code>mutual</code> inference is possible:</p>
<pre> <span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-keyword">let</span> <span class="agda2-highlight-bound-variable">i</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-symbol">λ</span> <span class="agda2-highlight-bound-variable">x</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">x</span> <span class="agda2-highlight-keyword">in</span> <span class="agda2-highlight-bound-variable">i</span> <span class="agda2-highlight-inductive-constructor">true</span>
<span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-function">i</span> <span class="agda2-highlight-inductive-constructor">true</span> <span class="agda2-highlight-keyword">where</span> <span class="agda2-highlight-function">i</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-symbol">λ</span> <span class="agda2-highlight-bound-variable">x</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">x</span>
<span class="agda2-highlight-keyword">mutual</span>
<span class="agda2-highlight-function">i</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-symbol">λ</span> <span class="agda2-highlight-bound-variable">x</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">x</span>
<span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-function">i</span> <span class="agda2-highlight-inductive-constructor">true</span>
</pre>
<p>In general, definitions in a <code>let</code>/<code>where</code>/<code>mutual</code> block share the same context, which makes it possible to infer more things than with consecutive standalone definitions. It's occasionally useful to create a bogus <code>mutual</code> block when you want the type of a definition to be inferred based on its use.</p>
<h2 id="unification-intro">Unification intro</h2>
<pre><span class="agda2-highlight-keyword">module</span> <span class="agda2-highlight-module">UnificationIntro</span> <span class="agda2-highlight-keyword">where</span>
</pre>
<p>The following definitions type check:</p>
<pre> <span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-symbol">(λ</span> <span class="agda2-highlight-bound-variable">x</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">x</span><span class="agda2-highlight-symbol">)</span> <span class="agda2-highlight-number">1</span>
<span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-symbol">(λ</span> <span class="agda2-highlight-bound-variable">x</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-number">2</span><span class="agda2-highlight-symbol">)</span> <span class="agda2-highlight-number">1</span>
</pre>
<p>reassuring that Agda's type checker is not based on some simple bidirectional typing rules (if you're not familier with those, see <a href="http://www.davidchristiansen.dk/tutorials/bidirectional.pdf">Bidirectional Typing Rules: A Tutorial</a>), but the type checker does have a bidirectional interface (<a href="https://hackage.haskell.org/package/Agda-2.6.1/docs/Agda-TheTypeChecker.html#v:inferExpr"><code>inferExpr</code></a> & <a href="https://hackage.haskell.org/package/Agda-2.6.1/docs/Agda-TheTypeChecker.html#v:checkExpr"><code>checkExpr</code></a>) where type inference is defined in terms of type checking for the most part:</p>
<pre><code> -- | Infer the type of an expression. Implemented by checking against a meta variable. <...>
inferExpr :: A.Expr -> TCM (Term, Type)</code></pre>
<p>which means that any definition of the following form:</p>
<pre><code> name = term</code></pre>
<p>can be equally written as</p>
<pre><code> name : _
name = term</code></pre>
<p>since Agda elaborates <code>_</code> to a fresh metavariable and then type checks <code>term</code> against it, which amounts to unifying the inferred type of <code>term</code> with the meta. If the inferred type doesn't contain metas itself, then the meta standing for <code>_</code> is resolved as that type and the definition is accepted (if the inferred type does contain metas, things get more difficult and we're not going to describe all the gory details here). So type inference is just a particular form of unification.</p>
<p>You can put <code>_</code> basically anywhere and let Agda infer what term/type it stands for. For example:</p>
<pre> <span class="agda2-highlight-function">id₂</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-primitive-type">Set</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-symbol">_</span>
<span class="agda2-highlight-function">id₂</span> <span class="agda2-highlight-bound-variable">x</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-bound-variable">x</span>
</pre>
<p>Here Agda binds the <code>x</code> variable and records that it has type <code>A</code> and when the <code>x</code> variable is returned as a result, Agda unifies the expected type <code>_</code> with the actual type of <code>x</code>, which is <code>A</code>. Thus the definition above elaborates to</p>
<pre> <span class="agda2-highlight-function">id₂′</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-primitive-type">Set</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">A</span>
<span class="agda2-highlight-function">id₂′</span> <span class="agda2-highlight-bound-variable">x</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-bound-variable">x</span>
</pre>
<p>This definition:</p>
<pre> <span class="agda2-highlight-function">id₃</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-primitive-type">Set</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-symbol">_</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">A</span>
<span class="agda2-highlight-function">id₃</span> <span class="agda2-highlight-bound-variable">x</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-bound-variable">x</span>
</pre>
<p>elaborates to the same result in a similar fashion, except now Agda first records that the type of <code>x</code> is a meta and when <code>x</code> is returned as a result, Agda unifies that meta with the expected type, i.e. <code>A</code>, and so the meta gets resolved as <code>A</code>.</p>
<p>An <code>id</code> function that receives an explicit type:</p>
<pre> <span class="agda2-highlight-function">id₄</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-primitive-type">Set</span><span class="agda2-highlight-symbol">)</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-symbol">_</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">A</span>
<span class="agda2-highlight-function">id₄</span> <span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-bound-variable">x</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-bound-variable">x</span>
</pre>
<p>can be called as</p>
<pre> <span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-function">id₄</span> <span class="agda2-highlight-symbol">_</span> <span class="agda2-highlight-inductive-constructor">true</span>
</pre>
<p>and the <code>_</code> will be inferred as <code>Bool</code>.</p>
<p>It's also possible to explicitly specify an implicit type by <code>_</code>, which is essentially a no-op:</p>
<pre> <span class="agda2-highlight-function">id₅</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-primitive-type">Set</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">A</span>
<span class="agda2-highlight-function">id₅</span> <span class="agda2-highlight-bound-variable">x</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-bound-variable">x</span>
<span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-function">id₅</span> <span class="agda2-highlight-symbol">{_}</span> <span class="agda2-highlight-inductive-constructor">true</span>
</pre>
<h2 id="inference-and-pattern-matching">Inference and pattern matching</h2>
<pre><span class="agda2-highlight-keyword">module</span> <span class="agda2-highlight-module">InferenceAndPatternMatching</span> <span class="agda2-highlight-keyword">where</span>
</pre>
<p>Unrestricted pattern matching breaks type inference. Take for instance</p>
<pre> <span class="agda2-highlight-symbol"><span class="agda2-highlight-function"><span class="agda2-highlight-unsolved-meta">_</span></span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-symbol"><span class="agda2-highlight-unsolved-meta">λ</span></span><span class="agda2-highlight-unsolved-meta"> </span><span class="agda2-highlight-keyword"><span class="agda2-highlight-unsolved-meta">where</span></span>
<span class="agda2-highlight-inductive-constructor"><span class="agda2-highlight-unsolved-meta">zero</span></span><span class="agda2-highlight-unsolved-meta"> </span><span class="agda2-highlight-symbol"><span class="agda2-highlight-unsolved-meta">-></span></span><span class="agda2-highlight-unsolved-meta"> </span><span class="agda2-highlight-inductive-constructor"><span class="agda2-highlight-unsolved-meta">true</span></span>
<span class="agda2-highlight-symbol"><span class="agda2-highlight-unsolved-meta">(</span></span><span class="agda2-highlight-inductive-constructor"><span class="agda2-highlight-unsolved-meta">suc</span></span><span class="agda2-highlight-unsolved-meta"> </span><span class="agda2-highlight-symbol"><span class="agda2-highlight-unsolved-meta">_)</span></span><span class="agda2-highlight-unsolved-meta"> </span><span class="agda2-highlight-symbol"><span class="agda2-highlight-unsolved-meta">-></span></span><span class="agda2-highlight-unsolved-meta"> </span><span class="agda2-highlight-inductive-constructor"><span class="agda2-highlight-unsolved-meta">false</span></span>
</pre>
<p>which is a direct counterpart of Haskell's</p>
<pre><code> isZero = \case
0 -> True
_ -> False</code></pre>
<p>The latter is accepted by Haskell, but the former is not accepted by Agda: Agda colors the entire snippet in yellow meaning it's unable to resolve the generated metavariables. "What's the problem? The inferred type should be just <code>ℕ -> Bool</code>" -- you might think. Such a type works indeed:</p>
<pre> <span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-datatype">ℕ</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-datatype">Bool</span>
<span class="agda2-highlight-symbol">_</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-symbol">λ</span> <span class="agda2-highlight-keyword">where</span>
<span class="agda2-highlight-inductive-constructor">zero</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-inductive-constructor">true</span>
<span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-inductive-constructor">suc</span> <span class="agda2-highlight-symbol">_)</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-inductive-constructor">false</span>
</pre>
<p>But here's another thing that works:</p>
<pre> <span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-bound-variable">n</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-datatype">ℕ</span><span class="agda2-highlight-symbol">)</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">n</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-function">&</span></span> <span class="agda2-highlight-symbol">λ</span> <span class="agda2-highlight-keyword">where</span>
<span class="agda2-highlight-inductive-constructor">zero</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-datatype">Bool</span>
<span class="agda2-highlight-symbol"><span class="agda2-highlight-catchall-clause">_</span></span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-datatype">Bool</span>
<span class="agda2-highlight-symbol">_</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-symbol">λ</span> <span class="agda2-highlight-keyword">where</span>
<span class="agda2-highlight-inductive-constructor">zero</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-inductive-constructor">true</span>
<span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-inductive-constructor">suc</span> <span class="agda2-highlight-symbol">_)</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-inductive-constructor">false</span>
</pre>
<p>Recall that we're in a dependently typed language and here the type of the result of a function can depend on the argument of that function. And both the</p>
<pre><code> ℕ -> Bool
(n : ℕ) -> n & λ where
zero -> Bool
_ -> Bool</code></pre>
<p>types are correct for that function. Even though they are "morally" the same, they are not definitionally equal and there's a huge difference between them: the former one doesn't have a dependency and the latter one has.</p>
<p>There is a way to tell Agda that pattern matching is non-dependent: use <code>case_of_</code>, e.g.</p>
<pre> <span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-symbol">λ</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-bound-variable">n</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-datatype">ℕ</span><span class="agda2-highlight-symbol">)</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-operator"><span class="agda2-highlight-function">case</span></span> <span class="agda2-highlight-bound-variable">n</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-function">of</span></span> <span class="agda2-highlight-symbol">λ</span> <span class="agda2-highlight-keyword">where</span>
<span class="agda2-highlight-inductive-constructor">zero</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-inductive-constructor">true</span>
<span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-inductive-constructor">suc</span> <span class="agda2-highlight-symbol">_)</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-inductive-constructor">false</span>
</pre>
<p>type checks. <code>case_of_</code> is just a definition in the standard library that at the term level is essentially</p>
<pre><code> case x of f = f x</code></pre>
<p>and at the type level it restricts the type of <code>f</code> to be a non-dependent function.</p>
<p>Analogously, this is yellow:</p>
<pre> <span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-symbol">λ</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-bound-variable">n</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-datatype">ℕ</span><span class="agda2-highlight-symbol">)</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">n</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-function"><span class="agda2-highlight-unsolved-meta">&</span></span></span> <span class="agda2-highlight-symbol">λ</span> <span class="agda2-highlight-keyword">where</span>
<span class="agda2-highlight-inductive-constructor">zero</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-unsolved-constraint"><span class="agda2-highlight-unsolved-meta"><span class="agda2-highlight-inductive-constructor">true</span></span></span>
<span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-inductive-constructor">suc</span> <span class="agda2-highlight-symbol">_)</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-unsolved-constraint"><span class="agda2-highlight-unsolved-meta"><span class="agda2-highlight-inductive-constructor">false</span></span></span>
</pre>
<p>due to <code>_&_</code> being dependent:</p>
<pre><code> _&_ : {A : Set} {B : A -> Set} -> ∀ x -> (∀ x -> B x) -> B x
x & f = f x</code></pre>
<p>While this is fine:</p>
<pre> <span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-symbol">λ</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-bound-variable">n</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-datatype">ℕ</span><span class="agda2-highlight-symbol">)</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">n</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-function">&′</span></span> <span class="agda2-highlight-symbol">λ</span> <span class="agda2-highlight-keyword">where</span>
<span class="agda2-highlight-inductive-constructor">zero</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-inductive-constructor">true</span>
<span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-inductive-constructor">suc</span> <span class="agda2-highlight-symbol">_)</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-inductive-constructor">false</span>
</pre>
<p>due to <code>_&′_</code> being non-dependent:</p>
<pre><code> _&′_ : {A B : Set} -> A -> (A -> B) -> B
x &′ f = f x</code></pre>
<p>Agda's stdlib provides several intentionally non-dependent functions (e.g. <code>_∘′_</code>, <code>_$′_</code> and <code>case_of_</code> that we've already seen) to enable the user to get improved inference in the non-dependent case.</p>
<p>Note that annotating <code>n</code> with its type, <code>ℕ</code>, is mandatory in all the cases above. Agda is not able to conclude that if a value is matched against a pattern, then the value must have the same type as the pattern.</p>
<p>Even this doesn't type check:</p>
<pre> <span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-symbol"><span class="agda2-highlight-unsolved-meta">λ</span></span><span class="agda2-highlight-unsolved-meta"> </span><span class="agda2-highlight-bound-variable"><span class="agda2-highlight-unsolved-meta">n</span></span><span class="agda2-highlight-unsolved-meta"> </span><span class="agda2-highlight-symbol"><span class="agda2-highlight-unsolved-meta">-></span></span><span class="agda2-highlight-unsolved-meta"> </span><span class="agda2-highlight-operator"><span class="agda2-highlight-function"><span class="agda2-highlight-unsolved-meta">case</span></span></span><span class="agda2-highlight-unsolved-meta"> </span><span class="agda2-highlight-bound-variable"><span class="agda2-highlight-unsolved-meta">n</span></span><span class="agda2-highlight-unsolved-meta"> </span><span class="agda2-highlight-operator"><span class="agda2-highlight-function"><span class="agda2-highlight-unsolved-meta">of</span></span></span><span class="agda2-highlight-unsolved-meta"> </span><span class="agda2-highlight-symbol"><span class="agda2-highlight-unsolved-meta">λ</span></span><span class="agda2-highlight-unsolved-meta"> </span><span class="agda2-highlight-keyword"><span class="agda2-highlight-unsolved-meta">where</span></span>
<span class="agda2-highlight-inductive-constructor"><span class="agda2-highlight-unsolved-meta">zero</span></span><span class="agda2-highlight-unsolved-meta"> </span><span class="agda2-highlight-symbol"><span class="agda2-highlight-unsolved-meta">-></span></span><span class="agda2-highlight-unsolved-meta"> </span><span class="agda2-highlight-inductive-constructor"><span class="agda2-highlight-unsolved-meta">zero</span></span>
<span class="agda2-highlight-symbol"><span class="agda2-highlight-unsolved-meta">(</span></span><span class="agda2-highlight-inductive-constructor"><span class="agda2-highlight-unsolved-meta">suc</span></span><span class="agda2-highlight-unsolved-meta"> </span><span class="agda2-highlight-bound-variable"><span class="agda2-highlight-unsolved-meta">n</span></span><span class="agda2-highlight-symbol"><span class="agda2-highlight-unsolved-meta">)</span></span><span class="agda2-highlight-unsolved-meta"> </span><span class="agda2-highlight-symbol"><span class="agda2-highlight-unsolved-meta">-></span></span><span class="agda2-highlight-unsolved-meta"> </span><span class="agda2-highlight-bound-variable"><span class="agda2-highlight-unsolved-meta">n</span></span>
</pre>
<p>even though Agda really could figure out that if <code>zero</code> is returned from one of the branches, then the type of the result is <code>ℕ</code>, and since <code>n</code> is returned from the other branch and pattern matching is non-dependent, <code>n</code> must have the same type. See <a href="https://github.com/agda/agda/issues/2834">#2834</a> for why Agda doesn't attempt to be clever here.</p>
<p>There's a funny syntactical way to tell Agda that a function is non-dependent: just do not bind a variable at the type level. This type checks:</p>
<pre> <span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-datatype">ℕ</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-symbol">_</span>
<span class="agda2-highlight-symbol">_</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-symbol">λ</span> <span class="agda2-highlight-keyword">where</span>
<span class="agda2-highlight-inductive-constructor">zero</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-inductive-constructor">true</span>
<span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-inductive-constructor">suc</span> <span class="agda2-highlight-symbol">_)</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-inductive-constructor">false</span>
</pre>
<p>while this doesn't:</p>
<pre> <span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-bound-variable">n</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-datatype">ℕ</span><span class="agda2-highlight-symbol">)</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-symbol"><span class="agda2-highlight-unsolved-meta">_</span></span>
<span class="agda2-highlight-symbol">_</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-symbol">λ</span> <span class="agda2-highlight-keyword">where</span>
<span class="agda2-highlight-inductive-constructor">zero</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-unsolved-constraint"><span class="agda2-highlight-unsolved-meta"><span class="agda2-highlight-inductive-constructor">true</span></span></span>
<span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-inductive-constructor">suc</span> <span class="agda2-highlight-symbol">_)</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-unsolved-constraint"><span class="agda2-highlight-unsolved-meta"><span class="agda2-highlight-inductive-constructor">false</span></span></span>
</pre>
<p>In the latter case Agda treats <code>_</code> as being potentially dependent on <code>n</code>, since <code>n</code> is explicitly bound. And in the former case there can't be any dependency on a non-existing variable.</p>
<h2 id="inference-and-constructors">Inference and constructors</h2>
<pre><span class="agda2-highlight-keyword">module</span> <span class="agda2-highlight-module">InferenceAndConstructors</span> <span class="agda2-highlight-keyword">where</span>
</pre>
<p>Since tuples are dependent, this</p>
<pre> <span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-number">1</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-inductive-constructor"><span class="agda2-highlight-unsolved-meta">,</span></span></span> <span class="agda2-highlight-unsolved-constraint"><span class="agda2-highlight-unsolved-meta"><span class="agda2-highlight-number">2</span></span></span><span class="agda2-highlight-symbol">)</span>
</pre>
<p>results in unresolved metas as all of these</p>
<pre><code> ℕ × ℕ
Σ ℕ λ where
zero -> ℕ
_ -> ℕ
Σ ℕ λ where
1 -> ℕ
_ -> Bool</code></pre>
<p>are valid types for this expression, which is similar to what we've considered in the previous section, except here not all of the types are "morally the same": the last one is very different to the first two.</p>
<p>As in the case of functions you can use a non-dependent alternative</p>
<pre> <span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-number">1</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-function">,′</span></span> <span class="agda2-highlight-number">2</span><span class="agda2-highlight-symbol">)</span>
</pre>
<p>(<code>_,′_</code> is a non-dependent version of <code>_,_</code>)</p>
<p>to tell Agda not to worry about potential dependencies.</p>
<h2 id="implicit-arguments">Implicit arguments</h2>
<pre><span class="agda2-highlight-keyword">module</span> <span class="agda2-highlight-module">ImplicitArgumens</span> <span class="agda2-highlight-keyword">where</span>
</pre>
<p>As we've seen implicit arguments and metavariables are closely related. Agda's internal theory has metas in it, so inference of implicit arguments amounts to turning an implicit into a metavariable and resolving it later. The complicated part however is that it's not completely obvious where implicits get inserted.</p>
<p>For example, it may come as a surprise, but</p>
<pre><code> _ : ∀ {A : Set} -> A -> A
_ = λ {A : Set} x -> x</code></pre>
<p>gives a type error. This is because Agda greedily binds implicits, so the <code>A</code> at the term level gets automatically bound on the lhs (left-hand side, i.e. before <code>=</code>), which gives you essentially this:</p>
<pre><code> _ : ∀ {A : Set} -> A -> A
_ {_} = <your_code_goes_here></code></pre>
<p>where <code>{_}</code> stands for <code>{A}</code>. So you can't bind <code>A</code> by a lambda, because it's already silently bound for you. Although it's impossible to reference that type variable unless you explicitly name it as in</p>
<pre> <span class="agda2-highlight-function">id</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-primitive-type">Set</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">A</span>
<span class="agda2-highlight-function">id</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">A</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-symbol">λ</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-bound-variable">x</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-bound-variable">A</span><span class="agda2-highlight-symbol">)</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">x</span>
</pre>
<p>Not only does Agda eagerly binds implicits, but it also inserts them eagerly at the call site. E.g.</p>
<pre> <span class="agda2-highlight-function">id-id</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-primitive-type">Set</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">A</span>
<span class="agda2-highlight-function">id-id</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-function">id</span> <span class="agda2-highlight-function">id</span>
</pre>
<p>elaborates to</p>
<pre> <span class="agda2-highlight-function">id-id₁</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-primitive-type">Set</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">A</span>
<span class="agda2-highlight-function">id-id₁</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">A</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-function">id</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">A</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-function">id</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">A</span><span class="agda2-highlight-symbol">})</span>
</pre>
<p>I.e. the inner <code>id</code> gets implicitly instantiated and only then fed to the outer <code>id</code>. Hence the outer <code>id</code> is instantiated at <code>A -> A</code>, which is the type of the inner instantiated <code>id</code>.</p>
<p>An alternative could be</p>
<pre><code> id-id₂ : {A : Set} -> A -> A
id-id₂ {A} = id { {A : Set} -> A -> A } id {A}</code></pre>
<p>Here the inner <code>id</code> doesn't get instantiated and gets fed to the outer <code>id</code> as is. Hence the outer <code>id</code> is instantiated at <code>{A : Set} -> A -> A</code>, which is the type of the inner uninstantiated <code>id</code>.</p>
<p>(Except that definition does not type check, because <code>{A : Set} -> A -> A</code> is of type <code>Set₁</code> rather than <code>Set</code> and we don't bother fixing this with proper universe polymorphism as those details are irrelevant for explaining how implicits get inserted)</p>
<p>Eager insertion of implicits is the reason why Agda infers the type of <code>[]</code> as <code>List _A_42</code>: <code>[]</code> gets elaborated to <code>[] {_}</code>, because the explicit argument <code>A</code> of <code>List</code> is implicit for the constructors of <code>List</code> (i.e. <code>[]</code> and <code>_∷_</code>) and that implicit gets eagerly inserted.</p>
<p>One exception to the general rule that implicits get bound and inserted eagerly is aliases: a definition of the form <code><name1> = <name2></code> doesn't need a type signature (as we saw before with the <code>_∘ = _∘_</code> example) and gets accepted as is regardless of whether <code><name2></code> has any leading implicit arguments or not. Basically, <code><name1></code> inherits its type signature from <code><name2></code> without any further elaboration.</p>
<p>There is a notorious bug related to insertion of implicit lambdas that has been in Agda for ages (even since its creation probably?) called The Hidden Lambda Bug. I'm not going to describe the bug here as details change across different version of Agda, but here are some links:</p>
<ul>
<li>tracked in <a href="https://github.com/agda/agda/issues/1079">this issue</a></li>
<li>discussed in detail in <a href="https://github.com/agda/agda/issues/2099">this issue</a></li>
<li>there's even an entire <a href="http://www2.tcs.ifi.lmu.de/~abel/MScThesisJohanssonLloyd.pdf">MSc thesis</a> about it</li>
<li>and a <a href="https://github.com/AndrasKovacs/implicit-fun-elaboration/blob/master/paper.pdf">plausible solution</a></li>
</ul>
<p>So while Agda's elaborations works well, it has its edge cases. In practice, it's not a big deal to insert an implicit lambda to circumvent the bug, but it's not always clear that Agda throws a type error because of this bug and not due to something else (e.g. I was completely lost in <a href="https://github.com/agda/agda/issues/1095">this case</a>). So beware.</p>
<h2 id="an-underspecified-argument-example">An underspecified argument example</h2>
<pre><span class="agda2-highlight-keyword">module</span> <span class="agda2-highlight-module">UnderspecifiedArgument</span> <span class="agda2-highlight-keyword">where</span>
</pre>
<p>Another difference between Haskell and Agda is that Agda is not happy about ambiguous types that don't really affect anything. Consider a classic example: the <code>I</code> combinator can be defined in terms of the <code>S</code> and <code>K</code> combinators. In Haskell we can express that as</p>
<pre><code> k :: a -> b -> a
k x y = x
s :: (a -> b -> c) -> (a -> b) -> a -> c
s f g x = f x (g x)
i :: a -> a
i = s k k</code></pre>
<p>and <a href="https://ideone.com/mZQM1f">it'll type check</a>. However the Agda's equivalent</p>
<pre> <span class="agda2-highlight-function">K</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-bound-variable">B</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-primitive-type">Set</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">B</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">A</span>
<span class="agda2-highlight-function">K</span> <span class="agda2-highlight-bound-variable">x</span> <span class="agda2-highlight-bound-variable">y</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-bound-variable">x</span>
<span class="agda2-highlight-function">S</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-bound-variable">B</span> <span class="agda2-highlight-bound-variable">C</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-primitive-type">Set</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">B</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">C</span><span class="agda2-highlight-symbol">)</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">B</span><span class="agda2-highlight-symbol">)</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">C</span>
<span class="agda2-highlight-function">S</span> <span class="agda2-highlight-bound-variable">f</span> <span class="agda2-highlight-bound-variable">g</span> <span class="agda2-highlight-bound-variable">x</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-bound-variable">f</span> <span class="agda2-highlight-bound-variable">x</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-bound-variable">g</span> <span class="agda2-highlight-bound-variable">x</span><span class="agda2-highlight-symbol">)</span>
<span class="agda2-highlight-function">I</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-symbol">∀</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">A</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">A</span>
<span class="agda2-highlight-function">I</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-function">S</span> <span class="agda2-highlight-function">K</span> <span class="agda2-highlight-function"><span class="agda2-highlight-unsolved-meta">K</span></span>
</pre>
<p>results in the last <code>K</code> being highlighted in yellow (which means that not all metavariables were resolved). To see why, let's inline <code>S</code> and see if the problem persists:</p>
<pre> <span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-symbol">∀</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">A</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">A</span>
<span class="agda2-highlight-symbol">_</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-symbol">λ</span> <span class="agda2-highlight-bound-variable">x</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-function">K</span> <span class="agda2-highlight-bound-variable">x</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-function"><span class="agda2-highlight-unsolved-meta">K</span></span> <span class="agda2-highlight-bound-variable">x</span><span class="agda2-highlight-symbol">)</span>
</pre>
<p>It does. So the problem is that in the expression above the final <code>K x</code> argument is underspecified: a <code>K</code> must receive a particular <code>B</code>, but we neither explicitly specify a <code>B</code>, nor it can be inferred from the context as the entire <code>K x</code> argument is thrown away by the outer <code>K</code>.</p>
<p>To fix this we can explicitly specify a <code>B</code> (any of type <code>Set</code> will work, let's pick <code>ℕ</code>):</p>
<pre> <span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-symbol">∀</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">A</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">A</span>
<span class="agda2-highlight-symbol">_</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-function">S</span> <span class="agda2-highlight-function">K</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-function">K</span> <span class="agda2-highlight-symbol">{</span>B <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-datatype">ℕ</span><span class="agda2-highlight-symbol">})</span>
</pre>
<p>In general, Agda expects all implicits (and metavariables in general) to be resolved and won't gloss over such details the way Haskell does. Agda is a proof assistant and under the <a href="https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence">Curry-Howard correspondence</a> each argument to a function represents a certain logical assumption and every such assumption must be fulfilled at the call site either explicitly or in an automated manner.</p>
<h2 id="not-dependent-enough">Not dependent enough</h2>
<pre><span class="agda2-highlight-keyword">module</span> <span class="agda2-highlight-module">NotDependentEnough</span> <span class="agda2-highlight-keyword">where</span>
</pre>
<p>Speaking of <code>K</code>, what do you think its most general type is, in Agda? Recall that we were using this definition in the previous section:</p>
<pre> <span class="agda2-highlight-function">K₀</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-primitive-type">Set</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">B</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-primitive-type">Set</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">B</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">A</span>
<span class="agda2-highlight-function">K₀</span> <span class="agda2-highlight-bound-variable">x</span> <span class="agda2-highlight-bound-variable">y</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-bound-variable">x</span>
</pre>
<p>Looking at that type signature, we can think of making the type of the second argument dependent on the first argument:</p>
<pre> <span class="agda2-highlight-function">K₁</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-primitive-type">Set</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">B</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-primitive-type">Set</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-symbol">∀</span> <span class="agda2-highlight-bound-variable">x</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">B</span> <span class="agda2-highlight-bound-variable">x</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">A</span>
</pre>
<p>This version looks more general, but it's in fact not, as <code>K₁</code> can be expressed in terms of <code>K₀</code>:</p>
<pre> <span class="agda2-highlight-function">K₁</span> <span class="agda2-highlight-bound-variable">x</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-function">K₀</span> <span class="agda2-highlight-bound-variable">x</span>
</pre>
<p>Basically, if you have an <code>x</code> to pass to <code>K₀</code>, then you can use that same <code>x</code> to apply a <code>B : A -> Set</code> to it to get <code>B x</code> of type <code>Set</code> and since the non-dependent <code>K</code> does not restrict the type of its second argument in any way, <code>B x</code> is good enough, and the fact that it mentions the particular <code>x</code> being passed as a first term-level argument, is just irrelevant. If we fully spell it out:</p>
<pre> <span class="agda2-highlight-function">K₁′</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-primitive-type">Set</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">B</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-primitive-type">Set</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-symbol">∀</span> <span class="agda2-highlight-bound-variable">x</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">B</span> <span class="agda2-highlight-bound-variable">x</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">A</span>
<span class="agda2-highlight-function">K₁′</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">A</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">B</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-bound-variable">x</span> <span class="agda2-highlight-bound-variable">y</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-function">K₀</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">A</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">B</span> <span class="agda2-highlight-bound-variable">x</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-bound-variable">x</span> <span class="agda2-highlight-bound-variable">y</span>
</pre>
<p>Note that we had to eta-expand the definition of <code>K₁</code>. If we don't do that, we'll get an error:</p>
<pre><code> -- Cannot instantiate the metavariable _360 to solution B x
-- since it contains the variable x
-- which is not in scope of the metavariable
K₁ : {A : Set} {B : A -> Set} -> ∀ x -> B x -> A
K₁ = K₀</code></pre>
<p>This is because this definition of <code>K₁</code> elaborates to <code>K₁ {_} {_} = K₀ {_} {_}</code> due to eager insertion of implicits and the last <code>_</code> can't be resolved, because as we can see in <code>K₁′</code> it has to be <code>B x</code>, but <code>x</code> is not bound on the lhs and so Agda complains about it.</p>
<p><code>K₀</code> in turn can be expressed in terms of <code>K₁</code>:</p>
<pre> <span class="agda2-highlight-function">K₀-via-K₁</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-bound-variable">B</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-primitive-type">Set</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">B</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">A</span>
<span class="agda2-highlight-function">K₀-via-K₁</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-function">K₁</span>
</pre>
<p>Basically, <code>K₁</code> expects a <code>A -> Set</code> and we can create one from <code>B : Set</code> via <code>λ _ -> B</code>.</p>
<p>So <code>K₀</code> and <code>K₁</code> are equally powerful. And note how in both the <code>K₀</code>-via-<code>K₁</code> and <code>K₁</code>-via-<code>K₀</code> cases Agda successfully infers implicits.</p>
<p>So is <code>K₀</code>/<code>K₁</code> the best we can do? Nope, here's a twist: we can make the type of the result depend on the second argument (the one that gets dropped), which in turn requires to reflect the dependency in the type of the first argument (the one that gets returned), so we end up with</p>
<pre> <span class="comment">-- ᵈ for "dependent".</span>
<span class="agda2-highlight-function">Kᵈ</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-primitive-type">Set</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">B</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-primitive-type">Set</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-symbol">(∀</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">x</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">B</span> <span class="agda2-highlight-bound-variable">x</span><span class="agda2-highlight-symbol">)</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-symbol">∀</span> <span class="agda2-highlight-bound-variable">x</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">B</span> <span class="agda2-highlight-bound-variable">x</span>
<span class="agda2-highlight-function">Kᵈ</span> <span class="agda2-highlight-bound-variable">y</span> <span class="agda2-highlight-bound-variable">x</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-bound-variable">y</span>
</pre>
<p>Compare this to regular function application:</p>
<pre> <span class="agda2-highlight-function">apply</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-primitive-type">Set</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">B</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-primitive-type">Set</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-symbol">(∀</span> <span class="agda2-highlight-bound-variable">x</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">B</span> <span class="agda2-highlight-bound-variable">x</span><span class="agda2-highlight-symbol">)</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-symbol">∀</span> <span class="agda2-highlight-bound-variable">x</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">B</span> <span class="agda2-highlight-bound-variable">x</span>
<span class="agda2-highlight-function">apply</span> <span class="agda2-highlight-bound-variable">f</span> <span class="agda2-highlight-bound-variable">x</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-bound-variable">f</span> <span class="agda2-highlight-bound-variable">x</span>
</pre>
<p>I.e. <code>Kᵈ</code> is implicit function application.</p>
<p>"You're making it up! <code>Kᵈ</code> elaborates to <code>λ y x -> y {x}</code>, how is that a <code>K</code> combinator?"</p>
<p>Here is how: first of all, <code>K₀</code> can be directly defined via <code>Kᵈ</code>:</p>
<pre> <span class="agda2-highlight-function">K₀-via-Kᵈ</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-bound-variable">B</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-primitive-type">Set</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">B</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">A</span>
<span class="agda2-highlight-function">K₀-via-Kᵈ</span> <span class="agda2-highlight-bound-variable">x</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-function">Kᵈ</span> <span class="agda2-highlight-bound-variable">x</span>
</pre>
<p>But most importantly <code>Kᵈ</code> expresses the "drop the second argument, return the first one" idea better than than the non-dependent <code>K</code> as the former can be used where the latter fails. For example, in the <a href="http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.379.3169&rep=rep1&type=pdf">Outrageous but Meaningful Coincidences</a> paper the author stumbles upon a few expressions involving <code>K</code> that look like they should type check, but they don't, despite the fact that a bunch of very similar expressions also involving <code>K</code> type check perfectly well. So the author inlines the definition of <code>K</code> and writes in a footnote:</p>
<blockquote>
<p>It’s frankly astonishing how effective Agda’s implicit syntax mechanism turns out to be. The trouble is that the system’s limits are far from clear. It is hard to tell what shouldn’t work, and what is rather a lacuna.</p>
</blockquote>
<p>However in this case the problem is not with Agda not being able to infer something, but rather the type of <code>K</code> being too restrictive. If we use the dependent version of <code>K</code> instead, then <a href="https://github.com/effectfully/random-stuff/blob/07253f395c63813abb64a08045e22ae8412e5be6/Kipling.agda#L110-L114">everything type checks</a>.</p>
<p>Note that we had to eta-expand <code>K₀-via-Kᵈ</code>, but this time for a different reason. If we make it</p>
<pre><code> K₀-via-Kᵈ′ : {A B : Set} -> A -> B -> A
K₀-via-Kᵈ′ {A} {B} = {!Kᵈ {B} {λ _ -> A}!}</code></pre>
<p>and ask for the type of the expression in the hole, we'll see</p>
<pre><code> Goal: A -> B -> A
Have: ({B} -> A) -> B -> A</code></pre>
<p>and <code>A</code> and <code>{B} -> A</code> are two distinct types that fail to unify. While an expression of type <code>A</code> can be used wherever a <code>{B} -> A</code> is expected as Agda will realize that an implicit variable of type <code>B</code> can be simply ignored, and so this is why eta-expaning the definition solves the problem.</p>
<p>Is <code>Kᵈ</code> the best we can do? Well, Agda has explicit universe polymorphism, so we can and should make the definition universe-polymorphic:</p>
<pre> <span class="agda2-highlight-function">Kᵈ′</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-symbol">∀</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">α</span> <span class="agda2-highlight-bound-variable">β</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-primitive-type">Set</span> <span class="agda2-highlight-bound-variable">α</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">B</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-primitive-type">Set</span> <span class="agda2-highlight-bound-variable">β</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-symbol">(∀</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">x</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">B</span> <span class="agda2-highlight-bound-variable">x</span><span class="agda2-highlight-symbol">)</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-symbol">∀</span> <span class="agda2-highlight-bound-variable">x</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">B</span> <span class="agda2-highlight-bound-variable">x</span>
<span class="agda2-highlight-function">Kᵈ′</span> <span class="agda2-highlight-bound-variable">y</span> <span class="agda2-highlight-bound-variable">x</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-bound-variable">y</span>
</pre>
<p>Which gives us a reasonably general definition that works in most practical cases, but here's an example of where it fails:</p>
<pre><code> -- Set (lsuc (lsuc α)) != Set _β_382
-- when checking that the expression Set α has type Set (lsuc α)
_ = Kᵈ′ (λ {α} -> Set α)</code></pre>
<p>This is because the type of <code>Set α</code> is <code>Set (lsuc α)</code> where <code>α</code> is an (implicit) argument, i.e. the universe where <code>B</code> lies depends on the received value and <code>Kᵈ′</code> does not support this due to <code>β</code> not depending on an <code>A</code> in the type of <code>B</code>: <code>A -> Set β</code>.</p>
<p>We can support this use case by turning <code>β</code> into a function from <code>A</code>:</p>
<pre> <span class="agda2-highlight-function">Kᵈ′′</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-symbol">∀</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">α</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-primitive-type">Set</span> <span class="agda2-highlight-bound-variable">α</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">β</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-postulate">Level</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">B</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-symbol">∀</span> <span class="agda2-highlight-bound-variable">x</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-primitive-type">Set</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-bound-variable">β</span> <span class="agda2-highlight-bound-variable">x</span><span class="agda2-highlight-symbol">)}</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-symbol">(∀</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">x</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">B</span> <span class="agda2-highlight-bound-variable">x</span><span class="agda2-highlight-symbol">)</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-symbol">∀</span> <span class="agda2-highlight-bound-variable">x</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">B</span> <span class="agda2-highlight-bound-variable">x</span>
<span class="agda2-highlight-function">Kᵈ′′</span> <span class="agda2-highlight-bound-variable">y</span> <span class="agda2-highlight-bound-variable">x</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-bound-variable">y</span>
</pre>
<p>Now the example type checks:</p>
<pre> <span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-function">Kᵈ′′</span> <span class="agda2-highlight-symbol">(λ</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">α</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-primitive-type">Set</span> <span class="agda2-highlight-bound-variable">α</span><span class="agda2-highlight-symbol">)</span>
</pre>
<p>But that is rarely needed in practice and not making <code>β</code> a function is good enough most of the time.</p>
<p>In general, an attempt to apply a higher-order function expecting a non-dependent function as its argument to a dependent function results in an error talking about a variable not being in scope of a metavariable. As a quick example, having a random dependently typed function:</p>
<pre> <span class="agda2-highlight-function">BoolOrℕ</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-datatype">Bool</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-primitive-type">Set</span>
<span class="agda2-highlight-function">BoolOrℕ</span> <span class="agda2-highlight-inductive-constructor">true</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-datatype">Bool</span>
<span class="agda2-highlight-function">BoolOrℕ</span> <span class="agda2-highlight-inductive-constructor">false</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-datatype">ℕ</span>
<span class="agda2-highlight-function">falseOrZero</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-bound-variable">b</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-datatype">Bool</span><span class="agda2-highlight-symbol">)</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-function">BoolOrℕ</span> <span class="agda2-highlight-bound-variable">b</span>
<span class="agda2-highlight-function">falseOrZero</span> <span class="agda2-highlight-inductive-constructor">true</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-inductive-constructor">false</span>
<span class="agda2-highlight-function">falseOrZero</span> <span class="agda2-highlight-inductive-constructor">false</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-number">0</span>
</pre>
<p>we can trigger the error by trying to feed <code>falseOrZero</code> to <code>_$′_</code> (which expects a non-dependent function):</p>
<pre><code> -- Cannot instantiate the metavariable _401 to solution BoolOrℕ b
-- since it contains the variable b
-- which is not in scope of the metavariable
_ = falseOrZero $′ true</code></pre>
<p>The exact error message depends on the version of Agda used, though.</p>
<p>But note that</p>
<ol style="list-style-type: decimal">
<li>this error can be triggered in different cases as well, as we saw with <code>K₁ = K₀</code></li>
<li>applying a higher-order function to an unexpectedly dependent function can give a different error, as we saw with <code>Kᵈ′′ (λ {α} -> Set α)</code></li>
</ol>
<p>Anyway, in my experience being able to make sense of that particular error is really helpful.</p>
<h2 id="inferring-implicits">Inferring implicits</h2>
<pre><span class="agda2-highlight-keyword">module</span> <span class="agda2-highlight-module">InferringImplicits</span> <span class="agda2-highlight-keyword">where</span>
</pre>
<p>As we've seen previously the following code type checks fine:</p>
<pre> <span class="agda2-highlight-function">id</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-primitive-type">Set</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">A</span>
<span class="agda2-highlight-function">id</span> <span class="agda2-highlight-bound-variable">x</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-bound-variable">x</span>
<span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-function">id</span> <span class="agda2-highlight-inductive-constructor">true</span>
</pre>
<p>Here <code>A</code> is bound implicitly in <code>id</code>, but Agda is able to infer that in this case <code>A</code> should be instantiated to <code>Bool</code> and so Agda elaborates the expression to <code>id {Bool} true</code>.</p>
<p>This is something that Haskell would infer as well. The programmer would hate to explicitly write out the type of every single argument, so programming languages often allow the user not to specify types when they can be inferred from the context. Agda is quite unique here however, because it can infer a lot more than other languages (even similar dependently typed ones) due to bespoke machineries handling various common patterns. But let's start with the basics.</p>
<h2 id="arguments-of-data-types">Arguments of data types</h2>
<pre><span class="agda2-highlight-keyword">module</span> <span class="agda2-highlight-module">ArgumentsOfDataTypes</span> <span class="agda2-highlight-keyword">where</span>
<span class="agda2-highlight-keyword">open</span> <span class="agda2-highlight-module">BasicsOfTypeInference</span>
</pre>
<p>Agda can infer parameters/indices of a data type from a value of that data type. For example if you have a function</p>
<pre> <span class="agda2-highlight-function">listId</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-symbol">∀</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">A</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-datatype">List</span> <span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-datatype">List</span> <span class="agda2-highlight-bound-variable">A</span>
<span class="agda2-highlight-function">listId</span> <span class="agda2-highlight-bound-variable">xs</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-bound-variable">xs</span>
</pre>
<p>then the implicit <code>A</code> can be inferred from a list:</p>
<pre> <span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-function">listId</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-number">1</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-inductive-constructor">∷</span></span> <span class="agda2-highlight-number">2</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-inductive-constructor">∷</span></span> <span class="agda2-highlight-inductive-constructor">[]</span><span class="agda2-highlight-symbol">)</span>
</pre>
<p>Unless, of course, <code>A</code> can't be determined from the list alone. E.g. if we pass an empty list to <code>f</code>, Agda will mark <code>listId</code> with yellow and display an unresolved metavariable <code>_A</code>:</p>
<pre> <span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-function"><span class="agda2-highlight-unsolved-meta">listId</span></span> <span class="agda2-highlight-inductive-constructor">[]</span>
</pre>
<p>Another example of this situation is when the list is not empty, but the type of its elements can't be inferred, e.g.</p>
<pre> <span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-function">listId</span> <span class="agda2-highlight-symbol">((λ</span> <span class="agda2-highlight-bound-variable"><span class="agda2-highlight-unsolved-meta">x</span></span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">x</span><span class="agda2-highlight-symbol">)</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-inductive-constructor">∷</span></span> <span class="agda2-highlight-inductive-constructor">[]</span><span class="agda2-highlight-symbol">)</span>
</pre>
<p>Here the type of <code>x</code> can be essentially anything (<code>ℕ</code>, <code>List Bool</code>, <code>⊤ × Bool -> ℕ</code>, etc), so Agda asks to provide missing details. Which we can do either by supplying a value for the implicit argument explicitly</p>
<pre> <span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-function">listId</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-datatype">ℕ</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-datatype">ℕ</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">((λ</span> <span class="agda2-highlight-bound-variable">x</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">x</span><span class="agda2-highlight-symbol">)</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-inductive-constructor">∷</span></span> <span class="agda2-highlight-inductive-constructor">[]</span><span class="agda2-highlight-symbol">)</span>
</pre>
<p>or by annotating <code>x</code> with a type</p>
<pre> <span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-function">listId</span> <span class="agda2-highlight-symbol">((λ</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-bound-variable">x</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-datatype">ℕ</span><span class="agda2-highlight-symbol">)</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">x</span><span class="agda2-highlight-symbol">)</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-inductive-constructor">∷</span></span> <span class="agda2-highlight-inductive-constructor">[]</span><span class="agda2-highlight-symbol">)</span>
</pre>
<p>or just by providing a type signature</p>
<pre> <span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-datatype">List</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-datatype">ℕ</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-datatype">ℕ</span><span class="agda2-highlight-symbol">)</span>
<span class="agda2-highlight-symbol">_</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-function">listId</span> <span class="agda2-highlight-symbol">((λ</span> <span class="agda2-highlight-bound-variable">x</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">x</span><span class="agda2-highlight-symbol">)</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-inductive-constructor">∷</span></span> <span class="agda2-highlight-inductive-constructor">[]</span><span class="agda2-highlight-symbol">)</span>
</pre>
<p>All these definitions are equivalent.</p>
<p>So "<code>A</code> is inferrable from a <code>List A</code>" doesn't mean that you can pass any list in and magically synthesize the type of its elements -- only that if that type is already known at the call site, then you don't need to explicitly specify it to apply <code>listId</code> to the list as it'll be inferred for you. "Already known at the call site" doesn't mean that the type of elements needs to be inferrable -- sometimes it can be derived from the context, for example:</p>
<pre> <span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-inductive-constructor">suc</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-inductive-constructor">∷</span></span> <span class="agda2-highlight-function">listId</span> <span class="agda2-highlight-symbol">((λ</span> <span class="agda2-highlight-bound-variable">x</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">x</span><span class="agda2-highlight-symbol">)</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-inductive-constructor">∷</span></span> <span class="agda2-highlight-inductive-constructor">[]</span><span class="agda2-highlight-symbol">)</span>
</pre>
<p>The implicit <code>A</code> gets inferred here: since all elements of a list have the same type, the type of <code>λ x -> x</code> must be the same as the type of <code>suc</code>, which is known to be <code>ℕ -> ℕ</code>, hence the type of <code>λ x -> x</code> is also <code>ℕ -> ℕ</code>.</p>
<h3 id="comparison-to-haskell">Comparison to Haskell</h3>
<p>In Haskell it's also the case that <code>a</code> is inferrable form a <code>[a]</code>: when the programmer writes</p>
<pre><code>` sort :: Ord a => [a] -> [a]</code></pre>
<p>Haskell is always able to infer <code>a</code> from the given list (provided <code>a</code> is known at the call site: <code>sort []</code> is as meaningless in Haskell as it is in Agda) and thus figure out what the appropriate <code>Ord a</code> instance is. However, another difference between Haskell and Agda is that whenever Haskell sees that some implicit variables (i.e. those bound by <code>forall <list_of_vars> .</code>) can't be inferred in the general case, Haskell, unlike Agda, will complain. E.g. consider the following piece of code:</p>
<pre><code> {-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, TypeFamilies #-}
class C a b where
f :: a -> Int
instance b ~ () => C Bool b where
f _ = 0
main = print $ f True</code></pre>
<p>Even though at the call site (<code>f True</code>) <code>b</code> is determined via the <code>b ~ ()</code> constraint of the <code>C Bool b</code> instance and so there is no ambiguity, Haskell still complains about the definition of the <code>C</code> class itself:</p>
<pre><code> • Could not deduce (C a b0)
from the context: C a b
bound by the type signature for:
f :: forall a b. C a b => a -> Int
at prog.hs:6:3-15
The type variable ‘b0’ is ambiguous</code></pre>
<p>The type of the <code>f</code> function mentions the <code>b</code> variable in the <code>C a b</code> constraint, but that variable is not mentioned anywhere else and hence can't be inferred in the general case, so Haskell complains, because by default it wants all type variables to be inferrable upfront regardless of whether at the call site it would be possible to infer a variable in some cases or not. We can override the default behavior by enabling the <code>AllowAmbiguousTypes</code> extension, which makes the code type check without any additional changes.</p>
<p>Agda's unification capabilities are well above Haskell's ones, so Agda doesn't attempt to predict what can and can't be inferred and allows us to make anything implicit, deferring resolution problems to the call site (i.e. it's like having <code>AllowAmbiguousTypes</code> globally enabled in Haskell). In fact, you can make implicit even such things that are pretty much guaranteed to never have any chance of being inferred, for example</p>
<pre> <span class="agda2-highlight-function">const-zeroᵢ</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-datatype">ℕ</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-datatype">ℕ</span> <span class="comment">-- `{ℕ}` is a shorthand for `{_ : ℕ}`</span>
<span class="agda2-highlight-function">const-zeroᵢ</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-inductive-constructor">zero</span>
</pre>
<p>as even</p>
<pre> <span class="agda2-highlight-function">const-zeroᵢ′</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-datatype">ℕ</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-datatype">ℕ</span>
<span class="agda2-highlight-function">const-zeroᵢ′</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-function"><span class="agda2-highlight-unsolved-meta">const-zeroᵢ</span></span>
</pre>
<p>results in unresolved metas, because it elaborates to</p>
<pre> <span class="agda2-highlight-function">const-zeroᵢ′-elaborated</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-datatype">ℕ</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-datatype">ℕ</span>
<span class="agda2-highlight-function">const-zeroᵢ′-elaborated</span> <span class="agda2-highlight-symbol">{_}</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-function">const-zeroᵢ</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-symbol"><span class="agda2-highlight-unsolved-meta">_</span></span><span class="agda2-highlight-symbol">}</span>
</pre>
<p>(due to eager insertion of implicits) and the fact that there's a variable of type <code>ℕ</code> bound in the current scope (regardless of whether it's bound explicitly or implicitly) does not have any effect on how implicits get resolved in the body of the definition. Metavariable resolution does not come up with instantiations for metavariables at random by looking at the local or global scope, it only determines what instantiations are bound to be by solving unification problems that arise during type checking.</p>
<p>But note that even though a value of type <code>{ℕ} -> ℕ</code> is not very useful on its own, having such a value as an argument like this:</p>
<pre> <span class="agda2-highlight-function">at1</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-symbol">({</span><span class="agda2-highlight-datatype">ℕ</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-datatype">ℕ</span><span class="agda2-highlight-symbol">)</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-datatype">ℕ</span>
<span class="agda2-highlight-function">at1</span> <span class="agda2-highlight-bound-variable">f</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-bound-variable">f</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-number">1</span><span class="agda2-highlight-symbol">}</span>
</pre>
<p>can be useful occasionally, because it gives you an API where the caller can decide if they want to bind the additional implicit variable or not. Here's an example for each of the cases:</p>
<pre> <span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-function">at1</span> <span class="agda2-highlight-number">2</span>
<span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-function">at1</span> <span class="agda2-highlight-symbol">λ</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">n</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">n</span>
</pre>
<p>Thus, <a href="https://en.wikipedia.org/wiki/Covariance_and_contravariance_(computer_science)#Function_types">covariantly positioned</a> implicits that are not determined by explicit arguments can be handy for providing defaults or additional data that the caller is usually not interested in, but occasionally is, and so the data is hidden in an implicit.</p>
<p>By the way, if you do need to resolve things based on the current scope, then Agda has <a href="https://agda.readthedocs.io/en/latest/language/instance-arguments.html">instance arguments</a> for that (they are similar to Haskell's type classes, but do not obey <a href="http://blog.ezyang.com/2014/07/type-classes-confluence-coherence-global-uniqueness">global uniqueness of instances</a>, because <a href="https://github.com/AndrasKovacs/pny1-assignment/blob/292e0fc28d7c27b35240d4f9d014bdf4db3afc62/DepTC.md#4-coherent-classes-in-dependent-languages">it's hard</a>), for example</p>
<pre> <span class="agda2-highlight-function">const-zeroᵢᵢ</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-symbol">{{</span><span class="agda2-highlight-datatype">ℕ</span><span class="agda2-highlight-symbol">}}</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-datatype">ℕ</span>
<span class="agda2-highlight-function">const-zeroᵢᵢ</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-inductive-constructor">zero</span>
<span class="agda2-highlight-function">const-zeroᵢᵢ′</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-symbol">{{</span><span class="agda2-highlight-datatype">ℕ</span><span class="agda2-highlight-symbol">}}</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-datatype">ℕ</span>
<span class="comment">-- Explicitly inserting `{{_}}` just to show that there's no interference with how instance</span>
<span class="comment">-- arguments get inserted.</span>
<span class="agda2-highlight-function">const-zeroᵢᵢ′</span> <span class="agda2-highlight-symbol">{{_}}</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-function">const-zeroᵢᵢ</span>
</pre>
<p>does not result in unresolved metas.</p>
<h3 id="under-the-hood">Under the hood</h3>
<pre><span class="agda2-highlight-keyword">module</span> <span class="agda2-highlight-module">UnderTheHood</span> <span class="agda2-highlight-keyword">where</span>
<span class="agda2-highlight-keyword">open</span> <span class="agda2-highlight-module">BasicsOfTypeInference</span>
</pre>
<h4 id="example-1-listid-1-2">Example 1: <code>listId (1 ∷ 2 ∷ [])</code></h4>
<p>Returning to our <code>listId</code> example, when the user writes</p>
<pre> <span class="agda2-highlight-function">listId</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-symbol">∀</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">A</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-datatype">List</span> <span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-datatype">List</span> <span class="agda2-highlight-bound-variable">A</span>
<span class="agda2-highlight-function">listId</span> <span class="agda2-highlight-bound-variable">xs</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-bound-variable">xs</span>
<span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-function">listId</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-number">1</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-inductive-constructor">∷</span></span> <span class="agda2-highlight-number">2</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-inductive-constructor">∷</span></span> <span class="agda2-highlight-inductive-constructor">[]</span><span class="agda2-highlight-symbol">)</span>
</pre>
<p>here is what happens under the hood:</p>
<ol style="list-style-type: decimal">
<li>the implicit <code>A</code> gets instantiated as a metavariable <code>_A</code></li>
<li>the type of the instantiated <code>listId</code> becomes <code>List _A -> List _A</code></li>
<li><code>List _A</code> (what the instantiated <code>listId</code> expects as an argument) gets unified with <code>List ℕ</code> (the type of the actual argument). We'll write this as <code>List _A =?= List ℕ</code></li>
<li>From unification's point of view type constructors are injective, hence <code>List _A =?= List ℕ</code> simplifies to <code>_A =?= ℕ</code>, which immediately gets solved as <code>_A := ℕ</code></li>
</ol>
<p>And this is how Agda figures out that <code>A</code> gets instantiated by <code>ℕ</code>.</p>
<h4 id="example-2-suc-listid-λ-x---x">Example 2: <code>suc ∷ listId ((λ x -> x) ∷ [])</code></h4>
<p>Similarly, when the user writes</p>
<pre> <span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-inductive-constructor">suc</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-inductive-constructor">∷</span></span> <span class="agda2-highlight-function">listId</span> <span class="agda2-highlight-symbol">((λ</span> <span class="agda2-highlight-bound-variable">x</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">x</span><span class="agda2-highlight-symbol">)</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-inductive-constructor">∷</span></span> <span class="agda2-highlight-inductive-constructor">[]</span><span class="agda2-highlight-symbol">)</span>
</pre>
<ol style="list-style-type: decimal">
<li>the implicit <code>A</code> gets instantiated as a metavariable <code>_A</code></li>
<li>the type of the instantiated <code>listId</code> becomes <code>List _A -> List _A</code></li>
<li><code>List _A</code> (what the instantiated <code>listId</code> expects as an argument) gets unified with <code>List (_B -> _B)</code> (the type of the actual argument). <code>_B</code> is another metavariable. Recall that we don't know the type of <code>x</code> and hence we simply make it a meta</li>
<li><code>List _A</code> (this time the type of the result that <code>listId</code> returns) also gets unified with the expected type, which is <code>List (ℕ -> ℕ)</code>, because <code>suc</code> prepended to the result of the <code>listId</code> application is of this type</li>
<li><p>we get the following <a href="https://en.wikipedia.org/wiki/Unification_(computer_science)#Unification_problem,_solution_set">unification problem</a> consisting of two equations:</p>
<pre><code> List _A =?= List (_B -> _B)
List _A =?= List (ℕ -> ℕ)</code></pre></li>
<li><p>as before we can simplify the equations by stripping <code>List</code>s from both the sides of each of them:</p>
<pre><code> _A =?= _B -> _B
_A =?= ℕ -> ℕ</code></pre></li>
<li><p>the second equation gives us <code>A := ℕ -> ℕ</code> and it only remains to solve</p>
<pre><code> ℕ -> ℕ =?= _B -> _B</code></pre></li>
<li><p>which is easy: <code>_B := ℕ</code>. The full solution of the unification problem is</p>
<pre><code> _B := ℕ
_A := ℕ -> ℕ</code></pre></li>
</ol>
<h4 id="example-3-λ-xs---suc-listid-xs">Example 3: <code>λ xs -> suc ∷ listId xs</code></h4>
<p>When the user writes</p>
<pre> <span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-symbol">λ</span> <span class="agda2-highlight-bound-variable">xs</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-inductive-constructor">suc</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-inductive-constructor">∷</span></span> <span class="agda2-highlight-function">listId</span> <span class="agda2-highlight-bound-variable">xs</span>
</pre>
<ol style="list-style-type: decimal">
<li>the yet-unknown type of <code>xs</code> elaborates to a metavariable, say, <code>_LA</code></li>
<li>the implicit <code>A</code> of <code>listId</code> elaborates to a metavariable <code>_A</code></li>
<li><code>List _A</code> (what the instantiated <code>listId</code> expects as an argument) gets unified with <code>_LA</code> (the type of the actual argument)</li>
<li><code>List _A</code> (this time the type of the result that <code>listId</code> returns) also gets unified with the expected type, which is <code>ℕ -> ℕ</code>, because <code>suc</code> prepended to the result of the <code>listId</code> application is of this type</li>
<li><p>we get a unification problem consisting of two equations:</p>
<pre><code> List _A =?= _LA
List _A =?= List (ℕ -> ℕ)</code></pre></li>
<li><code>_A</code> gets solved as <code>_A := ℕ -> ℕ</code></li>
<li>and <code>_LA</code> gets solved as <code>_LA := List (ℕ -> ℕ)</code></li>
<li><p>so the final solution is</p>
<pre><code> _A := ℕ -> ℕ
_LA := List (ℕ -> ℕ)</code></pre></li>
</ol>
<p>But note that we could first resolve <code>_LA</code> as <code>List _A</code>, then resolve <code>_A</code> and then instantiate it in <code>List _A</code> (what <code>_LA</code> was resolved to), which would give us the same final solution.</p>
<p>In general, there are many possible routes that one can take when solving a unification problem, but some of them are less straightforward (and thus less efficient) than others. Such details are beyond the scope of this document, here we are only interested in unification problems that get generated during type checking and solutions to them. Arriving at those solutions is a pretty technical (and incredibly convoluted) thing.</p>
<h2 id="nicer-notation">Nicer notation</h2>
<p>In the previous section we were stripping <code>List</code> from both the sides of an equation. We were able to do this, because from the unification's point of view type constructors are injective (this has nothing to do with the <a href="https://github.com/agda/agda/blob/10d704839742c332dc85f1298b80068ce4db6693/test/Succeed/InjectiveTypeConstructors.agda"><code>--injective-type-constructors</code></a> pragma that <a href="https://lists.chalmers.se/pipermail/agda/2010/001526.html">makes Agda anti-classical</a>). I.e. <code>List A</code> uniquely determines <code>A</code>.</p>
<p>We'll denote "<code>X</code> uniquely determines <code>Y</code>" (the notation comes from the <a href="https://ncatlab.org/nlab/show/bidirectional+typechecking">bidirectional typechecking</a> discipline) as <code>X ⇉ Y</code>. So <code>List A ⇉ A</code>.</p>
<p>An explicitly provided argument (i.e. <code>x</code> in either <code>f x</code> or <code>f {x}</code>) uniquely determines the type of that argument. We'll denote that as <code>(x : A) ⇉ A</code>.</p>
<p>We'll denote "<code>X</code> does not uniquely determine <code>Y</code>" as <code>X !⇉ Y</code>.</p>
<p>We'll also abbreviate</p>
<pre><code> X ⇉ Y₁
X ⇉ Y₂
...
X ⇉ yₙ</code></pre>
<p>as</p>
<pre><code> X ⇉ Y₁ , Y₂ ... Yₙ</code></pre>
<p>(and similarly for <code>!⇉</code>).</p>
<p>We'll denote "<code>X</code> can be determined in the current context" by</p>
<pre><code> ⇉ X</code></pre>
<p>Finally, we'll have derivation trees like</p>
<pre><code> X Y
→→→→→→→→→→
Z₁ , Z₂ A
→→→→→→→→→→→→→→→→
B</code></pre>
<p>which reads as "if <code>X</code> and <code>Y</code> are determined in the current context, then it's possible to determine <code>Z₁</code> and <code>Z₂</code>, having which together with <code>A</code> determined in the current context, is enough to determine <code>B</code>".</p>
<h2 id="type-functions">Type functions</h2>
<pre><span class="agda2-highlight-keyword">module</span> <span class="agda2-highlight-module">TypeFunctions</span> <span class="agda2-highlight-keyword">where</span>
<span class="agda2-highlight-keyword">open</span> <span class="agda2-highlight-module">BasicsOfTypeInference</span>
</pre>
<p>Analogously to <code>listId</code> we can define <code>fId</code> that works for any <code>F : Set -> Set</code>, including <code>List</code>:</p>
<pre> <span class="agda2-highlight-function">fId</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-symbol">∀</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">F</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-primitive-type">Set</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-primitive-type">Set</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">A</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">F</span> <span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">F</span> <span class="agda2-highlight-bound-variable">A</span>
<span class="agda2-highlight-function">fId</span> <span class="agda2-highlight-bound-variable">a</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-bound-variable">a</span>
</pre>
<p>Unfortunately applying <code>fId</code> to a list without explicitly instantiating <code>F</code> as <code>List</code></p>
<pre> <span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-function"><span class="agda2-highlight-unsolved-meta">fId</span></span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-unsolved-constraint"><span class="agda2-highlight-unsolved-meta"><span class="agda2-highlight-number">1</span></span></span><span class="agda2-highlight-unsolved-constraint"><span class="agda2-highlight-unsolved-meta"> </span></span><span class="agda2-highlight-operator"><span class="agda2-highlight-inductive-constructor"><span class="agda2-highlight-unsolved-meta"><span class="agda2-highlight-unsolved-constraint">∷</span></span></span></span><span class="agda2-highlight-unsolved-constraint"><span class="agda2-highlight-unsolved-meta"> </span></span><span class="agda2-highlight-unsolved-constraint"><span class="agda2-highlight-unsolved-meta"><span class="agda2-highlight-number">2</span></span></span><span class="agda2-highlight-unsolved-constraint"><span class="agda2-highlight-unsolved-meta"> </span></span><span class="agda2-highlight-operator"><span class="agda2-highlight-inductive-constructor"><span class="agda2-highlight-unsolved-meta"><span class="agda2-highlight-unsolved-constraint">∷</span></span></span></span><span class="agda2-highlight-unsolved-constraint"><span class="agda2-highlight-unsolved-meta"> </span></span><span class="agda2-highlight-unsolved-constraint"><span class="agda2-highlight-unsolved-meta"><span class="agda2-highlight-inductive-constructor">[]</span></span></span><span class="agda2-highlight-symbol">)</span>
</pre>
<p>results in both <code>F</code> and <code>A</code> not being resolved. This might be surprising, but there is a good reason for this behavior: there are multiple ways <code>F</code> and <code>A</code> can be instantiated. Here's the solution that the user would probably have had in their mind:</p>
<pre><code> _F := List
_A := ℕ</code></pre>
<p>which is what a first-order unification engine would come up with. But Agda's unification engine is <a href="https://stackoverflow.com/a/2504347/3237465">higher-order</a> and so this solution is also valid:</p>
<pre><code> _F := λ _ -> List ℕ
_A := Bool</code></pre>
<p>i.e. <code>F</code> ignores <code>A</code> and just returns <code>List ℕ</code>:</p>
<pre> <span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-function">fId</span> <span class="agda2-highlight-symbol">{λ</span> <span class="agda2-highlight-symbol"><span class="agda2-highlight-bound-variable">_</span></span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-datatype">List</span> <span class="agda2-highlight-datatype">ℕ</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-datatype">Bool</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-number">1</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-inductive-constructor">∷</span></span> <span class="agda2-highlight-number">2</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-inductive-constructor">∷</span></span> <span class="agda2-highlight-inductive-constructor">[]</span><span class="agda2-highlight-symbol">)</span>
</pre>
<p>Given that there are two valid solutions, Agda does not pick one at random and instead reports that there's ambiguity.</p>
<p>Even if you specify <code>A = ℕ</code>, <code>F</code> still can be either <code>List</code> or <code>λ _ -> List ℕ</code>, so you have to specify <code>F</code> (and then the problem reduces to the one that we considered earlier, hence there is no need to also specify <code>A</code>):</p>
<pre> <span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-function">fId</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-datatype">List</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-number">1</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-inductive-constructor">∷</span></span> <span class="agda2-highlight-number">2</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-inductive-constructor">∷</span></span> <span class="agda2-highlight-inductive-constructor">[]</span><span class="agda2-highlight-symbol">)</span>
</pre>
<p>Therefore, <code>F A</code> (where <code>F</code> is a bound variable) uniquely determines neither <code>F</code> nor <code>A</code>, i.e. <code>F A !⇉ F , A</code>.</p>
<p><a href="https://github.com/andreasabel">Andreas Abel</a>'s commented:</p>
<blockquote>
<p>Future research could improve on unification via an analysis in which situation the chosen solution does not matter (however, I never got around to do this research).</p>
<p>The example you give is such an instance: it does not matter how we solve <code>_F _A =?= List ℕ</code>, because the solutions of <code>_F</code> and <code>_A</code> can never flow out of the expression <code>fId _F _A (1 ∷ 2 ∷ []) : _F _A</code>.</p>
</blockquote>
<h3 id="comparison-to-haskell-1">Comparison to Haskell</h3>
<p>A type application of a variable is injective in Haskell. I.e. unification of <code>f a</code> and <code>g b</code> (where <code>f</code> and <code>g</code> are type variables) forces unification of <code>a</code> and <code>b</code>, as well as unification of <code>f</code> and <code>g</code>. I.e. not only does <code>f a ⇉ a</code> hold for arbitrary type variable <code>f</code>, but also <code>f a ⇉ f</code>. This makes it possible to define functions like</p>
<pre><code> fmap :: Functor f => (a -> b) -> f a -> f b</code></pre>
<p>and use them without compulsively specifying <code>f</code> at the call site each time.</p>
<p>Haskell is able to infer <code>f</code>, because no analogue of Agda's <code>λ _ -> List ℕ</code> is possible in Haskell as its surface language doesn't have type lambdas. You can't pass a type family as <code>f</code> either. Therefore there exists only one solution for "unify <code>f a</code> with <code>List Int</code>" in Haskell and it's the expected one:</p>
<pre><code> f := List
a := Int</code></pre>
<p>For a type family <code>F</code> we have <code>F a !⇉ a</code> (just like in Agda), unless <code>F</code> is an <a href="https://gitlab.haskell.org/ghc/ghc/wikis/injective-type-families">injective type family</a>.</p>
<h2 id="data-constructors">Data constructors</h2>
<pre><span class="agda2-highlight-keyword">module</span> <span class="agda2-highlight-module">DataConstructors</span> <span class="agda2-highlight-keyword">where</span>
</pre>
<p>Data constructors are injective from the unification point of view and from the theoretical point of view as well (unlike type constructors). E.g. consider the type of vectors (a vector is a list whose length is statically known):</p>
<pre> <span class="agda2-highlight-keyword">infixr</span> <span class="agda2-highlight-number">5</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-inductive-constructor">_∷ᵥ_</span></span>
<span class="agda2-highlight-keyword">data</span> <span class="agda2-highlight-datatype">Vec</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-primitive-type">Set</span><span class="agda2-highlight-symbol">)</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-datatype">ℕ</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-primitive-type">Set</span> <span class="agda2-highlight-keyword">where</span>
<span class="agda2-highlight-inductive-constructor">[]ᵥ</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-datatype">Vec</span> <span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-number">0</span>
<span class="agda2-highlight-operator"><span class="agda2-highlight-inductive-constructor">_∷ᵥ_</span></span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-symbol">∀</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">n</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-datatype">Vec</span> <span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-bound-variable">n</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-datatype">Vec</span> <span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-inductive-constructor">suc</span> <span class="agda2-highlight-bound-variable">n</span><span class="agda2-highlight-symbol">)</span>
</pre>
<p>The <code>head</code> function is defined like that over <code>Vec</code>:</p>
<pre> <span class="agda2-highlight-function">headᵥ</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-symbol">∀</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-bound-variable">n</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-datatype">Vec</span> <span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-inductive-constructor">suc</span> <span class="agda2-highlight-bound-variable">n</span><span class="agda2-highlight-symbol">)</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">A</span>
<span class="agda2-highlight-function">headᵥ</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-bound-variable">x</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-inductive-constructor">∷ᵥ</span></span> <span class="agda2-highlight-symbol">_)</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-bound-variable">x</span>
</pre>
<p>I.e. we require an input vector to have at least one element and return that first element.</p>
<p><code>n</code> can be left implicit, because <code>suc n ⇉ n</code>. In general, for a constructor <code>C</code> the following holds:</p>
<pre><code> C x₁ x₂ ... xₙ ⇉ x₁ , x₂ ... xₙ</code></pre>
<p>A simple test:</p>
<pre> <span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-function">headᵥ</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-number">0</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-inductive-constructor">∷ᵥ</span></span> <span class="agda2-highlight-inductive-constructor">[]ᵥ</span><span class="agda2-highlight-symbol">)</span>
</pre>
<p>Here we pass a one-element vector to <code>headᵥ</code> and Agda succesfully infers the implicit <code>n</code> of <code>headᵥ</code> to be <code>0</code> (i.e. no elements in the vector apart from the first one).</p>
<p>During unification the implicit <code>n</code> gets instantiated to a metavariable, say, <code>_n</code>, and <code>suc _n</code> (the expected length of the vector) gets unified with <code>suc zero</code> (i.e. 1, the actual length of the vector), which amounts to unifying <code>_n</code> with <code>zero</code>, which immediately results in <code>n := zero</code>.</p>
<p>Instead of having a constant vector, we can have a vector of an unspecified length and infer that length by providing <code>n</code> to <code>headᵥ</code> explicitly, as in</p>
<pre> <span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-symbol">λ</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">n</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-bound-variable">xs</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-function">headᵥ</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-datatype">ℕ</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">n</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-bound-variable">xs</span>
</pre>
<p>The type of that definition is <code>∀ {n} -> Vec ℕ (suc n) -> ℕ</code>.</p>
<p>We started by binding two variables without specifying their types, but those got inferred from how arguments are used by <code>headᵥ</code>.</p>
<p>Note that <code>_⇉_</code> is transitive, i.e. if <code>X ⇉ Y</code> and <code>Y ⇉ Z</code>, then <code>X ⇉ Z</code>. For example, since <code>Vec A n ⇉ n</code> (due to <code>Vec</code> being a type constructor) and <code>suc n ⇉ n</code> (due to <code>suc</code> being a data constructor), we have <code>Vec A (suc n) ⇉ n</code> (by transitivity of <code>_⇉_</code>).</p>
<h2 id="reduction">Reduction</h2>
<p>If <code>X</code> reduces to <code>Y</code> (we'll denote that as <code>X ~> Y</code>) and <code>Y ⇉ Z</code>, then <code>X ⇉ Z</code>.</p>
<p>E.g. if we define an alternative version of <code>headᵥ</code> that uses <code>1 +_</code> instead of <code>suc</code>:</p>
<pre> <span class="agda2-highlight-function">headᵥ⁺</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-symbol">∀</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-bound-variable">n</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-datatype">Vec</span> <span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-number">1</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-primitive">+</span></span> <span class="agda2-highlight-bound-variable">n</span><span class="agda2-highlight-symbol">)</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-bound-variable">A</span>
<span class="agda2-highlight-function">headᵥ⁺</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-bound-variable">x</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-inductive-constructor">∷ᵥ</span></span> <span class="agda2-highlight-symbol">_)</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-bound-variable">x</span>
</pre>
<p>the <code>n</code> will still be inferrable:</p>
<pre> <span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-function">headᵥ⁺</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-number">0</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-inductive-constructor">∷ᵥ</span></span> <span class="agda2-highlight-inductive-constructor">[]ᵥ</span><span class="agda2-highlight-symbol">)</span>
</pre>
<p>This is because <code>1 + n</code> reduces to <code>suc n</code>, so the two definitions are equivalent.</p>
<p>Note however that a "morally" equivalent definition:</p>
<pre><code> headᵥ⁺-wrong : ∀ {A n} -> Vec A (n + 1) -> A
headᵥ⁺-wrong (x ∷ᵥ _) = x</code></pre>
<p>does not type check giving:</p>
<pre><code> I'm not sure if there should be a case for the constructor _∷ᵥ_,
because I get stuck when trying to solve the following unification
problems (inferred index ≟ expected index):
suc n ≟ n₁ + 1
when checking that the pattern x ∷ᵥ _ has type Vec A (n + 1)</code></pre>
<p>That's because <code>_+_</code> is defined by pattern matching on its left operand, so <code>1 + n</code> computes while <code>n + 1</code> is stuck and does not compute as <code>n</code> is a variable rather than an expression starting with a constructor of <code>ℕ</code>. <code>headᵥ⁺-wrong</code> is a contrived example, but this problem can arise in real cases, for example consider a naive attempt to define the <code>reverse</code> function over <code>Vec</code> using an accumulator, the helper type checks perfectly:</p>
<pre> <span class="agda2-highlight-function">reverse-go</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-symbol">∀</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-bound-variable">n</span> <span class="agda2-highlight-bound-variable">m</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-datatype">Vec</span> <span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-bound-variable">m</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-datatype">Vec</span> <span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-bound-variable">n</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-datatype">Vec</span> <span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-bound-variable">n</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-primitive">+</span></span> <span class="agda2-highlight-bound-variable">m</span><span class="agda2-highlight-symbol">)</span>
<span class="agda2-highlight-function">reverse-go</span> <span class="agda2-highlight-bound-variable">acc</span> <span class="agda2-highlight-inductive-constructor">[]ᵥ</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-bound-variable">acc</span>
<span class="agda2-highlight-function">reverse-go</span> <span class="agda2-highlight-bound-variable">acc</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-bound-variable">x</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-inductive-constructor">∷ᵥ</span></span> <span class="agda2-highlight-bound-variable">xs</span><span class="agda2-highlight-symbol">)</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-bound-variable">x</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-inductive-constructor">∷ᵥ</span></span> <span class="agda2-highlight-function">reverse-go</span> <span class="agda2-highlight-bound-variable">acc</span> <span class="agda2-highlight-bound-variable">xs</span>
</pre>
<p>but the final definition gives an error:</p>
<pre><code> -- _n_390 + 0 != n of type ℕ
reverse-wrong : ∀ {A n} -> Vec A n -> Vec A n
reverse-wrong xs = reverse-go []ᵥ xs</code></pre>
<p>That's because <code>reverse-go</code> is appled to <code>[]ᵥ</code> of type <code>Vec A 0</code> and <code>xs</code> of type <code>Vec A n</code>, so it returns a <code>Vec A (n + 0)</code>, which is not definitionally the same thing as <code>Vec A n</code>. We could prove that <code>n + 0</code> equals <code>n</code> for any <code>n</code> and use that proof to rewrite <code>Vec A (n + 0)</code> into <code>Vec A n</code>, but that would make it harder to prove properties about <code>reverse</code> defined this way.</p>
<p>The usual way of approaching this problem is by generalizing the helper. In the case of <code>reverse</code> we can generalize the helper to the regular <code>foldl</code> function and define <code>reverse</code> in terms of that -- that's what <a href="https://github.com/agda/agda-stdlib/blob/7c8c17b407c14c5828b8755abb7584a4878286da/src/Data/Vec/Base.agda#L270-L271">they do</a> in the standard library. See <a href="https://stackoverflow.com/questions/33345899/how-to-enumerate-the-elements-of-a-list-by-fins-in-linear-time">this Stack Overflow question and answer</a> for a more complex and elaborated example. Anyway, end of digression.</p>
<p>Agda looks under lambdas when reducing an expression, so for example <code>λ n -> 1 + n</code> and <code>λ n -> suc n</code> are two definitionally equal terms:</p>
<pre> <span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-symbol">(λ</span> <span class="agda2-highlight-bound-variable">n</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-number">1</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-primitive">+</span></span> <span class="agda2-highlight-bound-variable">n</span><span class="agda2-highlight-symbol">)</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-datatype">≡</span></span> <span class="agda2-highlight-symbol">(λ</span> <span class="agda2-highlight-bound-variable">n</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-inductive-constructor">suc</span> <span class="agda2-highlight-bound-variable">n</span><span class="agda2-highlight-symbol">)</span>
<span class="agda2-highlight-symbol">_</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-inductive-constructor">refl</span>
</pre>
<p>But Agda does not look under pattern matching lambdas, so for example these two functions</p>
<pre><code> λ{ zero -> zero; (suc n) -> 1 + n }
λ{ zero -> zero; (suc n) -> suc n }</code></pre>
<p>are not considered definitionally equal. In fact, even</p>
<pre><code> _ : _≡_ {A = ℕ -> ℕ}
(λ{ zero -> zero; (suc n) -> suc n })
(λ{ zero -> zero; (suc n) -> suc n })
_ = refl</code></pre>
<p>is an error despite the two functions being syntactically equal. Here's the funny error:</p>
<pre><code> (λ { zero → zero ; (suc n) → suc n }) x !=
(λ { zero → zero ; (suc n) → suc n }) x of type ℕ
when checking that the expression refl has type
(λ { zero → zero ; (suc n) → suc n }) ≡
(λ { zero → zero ; (suc n) → suc n })</code></pre>
<h2 id="pattern-matching">Pattern matching</h2>
<p>Generally speaking, pattern matching breaks inference. We'll consider various cases, but to start with the simplest ones we need to introduce a slightly weird definition of the plus operator:</p>
<pre><span class="agda2-highlight-keyword">module</span> <span class="agda2-highlight-module">WeirdPlus</span> <span class="agda2-highlight-keyword">where</span>
<span class="agda2-highlight-keyword">open</span> <span class="agda2-highlight-module">DataConstructors</span>
<span class="agda2-highlight-operator"><span class="agda2-highlight-function">_+′_</span></span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-datatype">ℕ</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-datatype">ℕ</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-datatype">ℕ</span>
<span class="agda2-highlight-inductive-constructor">zero</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-function">+′</span></span> <span class="agda2-highlight-bound-variable">m</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-bound-variable">m</span>
<span class="agda2-highlight-inductive-constructor">suc</span> <span class="agda2-highlight-bound-variable">n</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-function">+′</span></span> <span class="agda2-highlight-bound-variable">m</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-bound-variable">n</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-primitive">+</span></span> <span class="agda2-highlight-inductive-constructor">suc</span> <span class="agda2-highlight-bound-variable">m</span>
</pre>
<p>because the usual one</p>
<pre><code> _+_ : ℕ -> ℕ -> ℕ
zero + m = m
suc n + m = suc (n + m)</code></pre>
<p>is subject to certain unification heuristics, which the weird one doesn't trigger.</p>
<p>We'll be using the following function for demonstration purposes:</p>
<pre> <span class="agda2-highlight-function">idᵥ⁺</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-symbol">∀</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-bound-variable">n</span> <span class="agda2-highlight-bound-variable">m</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-datatype">Vec</span> <span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-bound-variable">n</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-function">+′</span></span> <span class="agda2-highlight-bound-variable">m</span><span class="agda2-highlight-symbol">)</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-datatype">Vec</span> <span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-bound-variable">n</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-function">+′</span></span> <span class="agda2-highlight-bound-variable">m</span><span class="agda2-highlight-symbol">)</span>
<span class="agda2-highlight-function">idᵥ⁺</span> <span class="agda2-highlight-bound-variable">xs</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-bound-variable">xs</span>
</pre>
<h3 id="a-constant-argument">A constant argument</h3>
<p><code>idᵥ⁺</code> applied to a constant vector</p>
<pre> <span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-function"><span class="agda2-highlight-unsolved-meta">idᵥ⁺</span></span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-unsolved-constraint"><span class="agda2-highlight-unsolved-meta"><span class="agda2-highlight-number">1</span></span></span><span class="agda2-highlight-unsolved-constraint"><span class="agda2-highlight-unsolved-meta"> </span></span><span class="agda2-highlight-operator"><span class="agda2-highlight-inductive-constructor"><span class="agda2-highlight-unsolved-meta"><span class="agda2-highlight-unsolved-constraint">∷ᵥ</span></span></span></span><span class="agda2-highlight-unsolved-constraint"><span class="agda2-highlight-unsolved-meta"> </span></span><span class="agda2-highlight-unsolved-constraint"><span class="agda2-highlight-unsolved-meta"><span class="agda2-highlight-number">2</span></span></span><span class="agda2-highlight-unsolved-constraint"><span class="agda2-highlight-unsolved-meta"> </span></span><span class="agda2-highlight-operator"><span class="agda2-highlight-inductive-constructor"><span class="agda2-highlight-unsolved-meta"><span class="agda2-highlight-unsolved-constraint">∷ᵥ</span></span></span></span><span class="agda2-highlight-unsolved-constraint"><span class="agda2-highlight-unsolved-meta"> </span></span><span class="agda2-highlight-unsolved-constraint"><span class="agda2-highlight-unsolved-meta"><span class="agda2-highlight-inductive-constructor">[]ᵥ</span></span></span><span class="agda2-highlight-symbol">)</span>
</pre>
<p>gives us yellow, because Agda turns the implicit <code>n</code> and <code>m</code> into metavariables <code>_n</code> and <code>_m</code> and tries to unify the expected length of a vector (<code>_n +′ _m</code>) with the actual one (<code>2</code>) and there are multiple solutions to this problem, e.g.</p>
<pre> <span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-function">idᵥ⁺</span> <span class="agda2-highlight-symbol">{</span>n <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-number">1</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">{</span>m <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-number">1</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-number">1</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-inductive-constructor">∷ᵥ</span></span> <span class="agda2-highlight-number">2</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-inductive-constructor">∷ᵥ</span></span> <span class="agda2-highlight-inductive-constructor">[]ᵥ</span><span class="agda2-highlight-symbol">)</span>
<span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-function">idᵥ⁺</span> <span class="agda2-highlight-symbol">{</span>n <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-number">2</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">{</span>m <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-number">0</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-number">1</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-inductive-constructor">∷ᵥ</span></span> <span class="agda2-highlight-number">2</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-inductive-constructor">∷ᵥ</span></span> <span class="agda2-highlight-inductive-constructor">[]ᵥ</span><span class="agda2-highlight-symbol">)</span>
</pre>
<p>Howewer as per the previous the section, we do not really need to specify <code>m</code>, since <code>_+′_</code> is defined by recursion on <code>n</code> and hence for it to reduce it suffices to specify only <code>n</code>:</p>
<pre> <span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-function">idᵥ⁺</span> <span class="agda2-highlight-symbol">{</span>n <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-number">1</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-number">1</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-inductive-constructor">∷ᵥ</span></span> <span class="agda2-highlight-number">2</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-inductive-constructor">∷ᵥ</span></span> <span class="agda2-highlight-inductive-constructor">[]ᵥ</span><span class="agda2-highlight-symbol">)</span>
</pre>
<p>since with <code>n</code> specified this way the <code>_n</code> metavariable gets resolved as <code>_n := 1</code> and the expected length of an argument, <code>_n +′ _m</code>, becomes <code>suc m</code>, which Agda knows how to unify with <code>2</code> (the length of the actual argument).</p>
<p>Specifying <code>m</code> instead of <code>n</code> won't work though:</p>
<pre> <span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-function"><span class="agda2-highlight-unsolved-meta">idᵥ⁺</span></span> <span class="agda2-highlight-symbol">{</span>m <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-number">1</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-unsolved-constraint"><span class="agda2-highlight-unsolved-meta"><span class="agda2-highlight-number">1</span></span></span><span class="agda2-highlight-unsolved-constraint"><span class="agda2-highlight-unsolved-meta"> </span></span><span class="agda2-highlight-operator"><span class="agda2-highlight-inductive-constructor"><span class="agda2-highlight-unsolved-meta"><span class="agda2-highlight-unsolved-constraint">∷ᵥ</span></span></span></span><span class="agda2-highlight-unsolved-constraint"><span class="agda2-highlight-unsolved-meta"> </span></span><span class="agda2-highlight-unsolved-constraint"><span class="agda2-highlight-unsolved-meta"><span class="agda2-highlight-number">2</span></span></span><span class="agda2-highlight-unsolved-constraint"><span class="agda2-highlight-unsolved-meta"> </span></span><span class="agda2-highlight-operator"><span class="agda2-highlight-inductive-constructor"><span class="agda2-highlight-unsolved-meta"><span class="agda2-highlight-unsolved-constraint">∷ᵥ</span></span></span></span><span class="agda2-highlight-unsolved-constraint"><span class="agda2-highlight-unsolved-meta"> </span></span><span class="agda2-highlight-unsolved-constraint"><span class="agda2-highlight-unsolved-meta"><span class="agda2-highlight-inductive-constructor">[]ᵥ</span></span></span><span class="agda2-highlight-symbol">)</span>
</pre>
<p>Agda can't resolve <code>_n</code>. This is because <code>_+′_</code> is defined by pattern matching on its first variable, so <code>1 +′ m</code> reduces to <code>suc m</code>, but <code>n +′ 1</code> is stuck and doesn't reduce to anything when <code>n</code> is a variable/metavariable/any stuck term. So even though there's a single solution to the</p>
<pre><code> n +′ 1 =?= 2</code></pre>
<p>unification problem, Agda is not able to come up with it, because this would require unbounded search in the general case and Agda's unification machinery carefully avoids any such strategies.</p>
<h3 id="a-non-constant-argument">A non-constant argument</h3>
<p><code>idᵥ⁺</code> applied to a non-constant vector has essentially the same inference properties.</p>
<p>Without specializing the implicit arguments we get yellow:</p>
<pre> <span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-symbol">λ</span> <span class="agda2-highlight-bound-variable">n</span> <span class="agda2-highlight-bound-variable">m</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-bound-variable">xs</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-datatype">Vec</span> <span class="agda2-highlight-datatype">ℕ</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-bound-variable">n</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-function">+′</span></span> <span class="agda2-highlight-bound-variable">m</span><span class="agda2-highlight-symbol">))</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-function"><span class="agda2-highlight-unsolved-meta">idᵥ⁺</span></span> <span class="agda2-highlight-unsolved-constraint"><span class="agda2-highlight-unsolved-meta"><span class="agda2-highlight-bound-variable">xs</span></span></span>
</pre>
<p>Specializing <code>m</code> doesn't help, still yellow:</p>
<pre> <span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-symbol">λ</span> <span class="agda2-highlight-bound-variable">n</span> <span class="agda2-highlight-bound-variable">m</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-bound-variable">xs</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-datatype">Vec</span> <span class="agda2-highlight-datatype">ℕ</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-bound-variable">n</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-function">+′</span></span> <span class="agda2-highlight-bound-variable">m</span><span class="agda2-highlight-symbol">))</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-function"><span class="agda2-highlight-unsolved-meta">idᵥ⁺</span></span> <span class="agda2-highlight-symbol">{</span>m <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-bound-variable">m</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-unsolved-constraint"><span class="agda2-highlight-unsolved-meta"><span class="agda2-highlight-bound-variable">xs</span></span></span>
</pre>
<p>And specializing <code>n</code> (with or without <code>m</code>) allows Agda to resolve all the metas:</p>
<pre> <span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-symbol">λ</span> <span class="agda2-highlight-bound-variable">n</span> <span class="agda2-highlight-bound-variable">m</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-bound-variable">xs</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-datatype">Vec</span> <span class="agda2-highlight-datatype">ℕ</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-bound-variable">n</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-function">+′</span></span> <span class="agda2-highlight-bound-variable">m</span><span class="agda2-highlight-symbol">))</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-function">idᵥ⁺</span> <span class="agda2-highlight-symbol">{</span>n <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-bound-variable">n</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-bound-variable">xs</span>
<span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-symbol">λ</span> <span class="agda2-highlight-bound-variable">n</span> <span class="agda2-highlight-bound-variable">m</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-bound-variable">xs</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-datatype">Vec</span> <span class="agda2-highlight-datatype">ℕ</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-bound-variable">n</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-function">+′</span></span> <span class="agda2-highlight-bound-variable">m</span><span class="agda2-highlight-symbol">))</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-function">idᵥ⁺</span> <span class="agda2-highlight-symbol">{</span>n <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-bound-variable">n</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-symbol">{</span>m <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-bound-variable">m</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-bound-variable">xs</span>
</pre>
<h3 id="examples">Examples</h3>
<p>So we have the following rule of thumb: whenever the type of function <code>h</code> mentions function <code>f</code> at the type level, every argument that gets pattern matched on in <code>f</code> (including any internal function calls) should be made explicit in <code>h</code> and every other argument can be left implicit (there are a few exceptions to this rule, which we'll consider below, but it applies in most cases).</p>
<h4 id="example-1-__">Example 1: <code>_+′_</code></h4>
<p><code>idᵥ⁺</code> mentions <code>_+′_</code> in its type:</p>
<pre><code> idᵥ⁺ : ∀ {A n m} -> Vec A (n +′ m) -> Vec A (n +′ m)</code></pre>
<p>and <code>_+′_</code> pattern matches on <code>n</code>, hence Agda won't be able to infer <code>n</code>, i.e. the user will have to provide it and so it should be made explicit:</p>
<pre><code> idᵥ⁺ : ∀ {A m} n -> Vec A (n +′ m) -> Vec A (n +′ m)</code></pre>
<p>Since <code>_+′_</code> doesn't match on its second argument, <code>m</code>, we leave it implicit.</p>
<h4 id="example-2-__">Example 2: <code>_∸_</code></h4>
<p>A function mentioning <code>_∸_</code></p>
<pre><code> _-_ : ℕ -> ℕ -> ℕ
n - zero = n
zero - suc m = zero
suc n - suc m = n - m</code></pre>
<p>at type level has to receive both the arguments that get fed to <code>_∸_</code> explicitly as <code>_∸_</code> matches on both of them:</p>
<pre> <span class="agda2-highlight-function">idᵥ⁻</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-symbol">∀</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">A</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-bound-variable">n</span> <span class="agda2-highlight-bound-variable">m</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-datatype">Vec</span> <span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-bound-variable">n</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-primitive">∸</span></span> <span class="agda2-highlight-bound-variable">m</span><span class="agda2-highlight-symbol">)</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-datatype">Vec</span> <span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-bound-variable">n</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-primitive">∸</span></span> <span class="agda2-highlight-bound-variable">m</span><span class="agda2-highlight-symbol">)</span>
<span class="agda2-highlight-function">idᵥ⁻</span> <span class="agda2-highlight-bound-variable">n</span> <span class="agda2-highlight-bound-variable">m</span> <span class="agda2-highlight-bound-variable">xs</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-bound-variable">xs</span>
</pre>
<p>and none of</p>
<pre> <span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-function">idᵥ⁻</span> <span class="agda2-highlight-number">2</span> <span class="agda2-highlight-symbol"><span class="agda2-highlight-unsolved-meta">_</span></span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-unsolved-constraint"><span class="agda2-highlight-unsolved-meta"><span class="agda2-highlight-number">1</span></span></span><span class="agda2-highlight-unsolved-constraint"><span class="agda2-highlight-unsolved-meta"> </span></span><span class="agda2-highlight-operator"><span class="agda2-highlight-inductive-constructor"><span class="agda2-highlight-unsolved-meta"><span class="agda2-highlight-unsolved-constraint">∷ᵥ</span></span></span></span><span class="agda2-highlight-unsolved-constraint"><span class="agda2-highlight-unsolved-meta"> </span></span><span class="agda2-highlight-unsolved-constraint"><span class="agda2-highlight-unsolved-meta"><span class="agda2-highlight-inductive-constructor">[]ᵥ</span></span></span><span class="agda2-highlight-symbol">)</span> <span class="comment">-- `m` can't be inferred</span>
<span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-function">idᵥ⁻</span> <span class="agda2-highlight-symbol"><span class="agda2-highlight-unsolved-meta">_</span></span> <span class="agda2-highlight-number">1</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-unsolved-constraint"><span class="agda2-highlight-unsolved-meta"><span class="agda2-highlight-number">1</span></span></span><span class="agda2-highlight-unsolved-constraint"><span class="agda2-highlight-unsolved-meta"> </span></span><span class="agda2-highlight-operator"><span class="agda2-highlight-inductive-constructor"><span class="agda2-highlight-unsolved-meta"><span class="agda2-highlight-unsolved-constraint">∷ᵥ</span></span></span></span><span class="agda2-highlight-unsolved-constraint"><span class="agda2-highlight-unsolved-meta"> </span></span><span class="agda2-highlight-unsolved-constraint"><span class="agda2-highlight-unsolved-meta"><span class="agda2-highlight-inductive-constructor">[]ᵥ</span></span></span><span class="agda2-highlight-symbol">)</span> <span class="comment">-- `n` can't be inferred</span>
</pre>
<p>is accepted unlike</p>
<pre> <span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-function">idᵥ⁻</span> <span class="agda2-highlight-number">2</span> <span class="agda2-highlight-number">1</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-number">1</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-inductive-constructor">∷ᵥ</span></span> <span class="agda2-highlight-inductive-constructor">[]ᵥ</span><span class="agda2-highlight-symbol">)</span>
</pre>
<h4 id="example-3-__">Example 3: <code>_*_</code></h4>
<p>A function mentioning <code>_*_</code></p>
<pre><code> _*_ : ℕ -> ℕ -> ℕ
zero * m = zero
suc n * m = m + n * m</code></pre>
<p>at the type level has to receive both the arguments that get fed to <code>_*_</code> explicitly, even though <code>_*_</code> doesn't directly match on <code>m</code>. This is because in the second clause <code>_*_</code> expands to <code>_+_</code>, which does match on <code>m</code>. So it's</p>
<pre> <span class="agda2-highlight-function">idᵥ*</span> <span class="agda2-highlight-symbol">:</span> <span class="agda2-highlight-symbol">∀</span> <span class="agda2-highlight-symbol">{</span><span class="agda2-highlight-bound-variable">A</span><span class="agda2-highlight-symbol">}</span> <span class="agda2-highlight-bound-variable">n</span> <span class="agda2-highlight-bound-variable">m</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-datatype">Vec</span> <span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-bound-variable">n</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-primitive">*</span></span> <span class="agda2-highlight-bound-variable">m</span><span class="agda2-highlight-symbol">)</span> <span class="agda2-highlight-symbol">-></span> <span class="agda2-highlight-datatype">Vec</span> <span class="agda2-highlight-bound-variable">A</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-bound-variable">n</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-primitive">*</span></span> <span class="agda2-highlight-bound-variable">m</span><span class="agda2-highlight-symbol">)</span>
<span class="agda2-highlight-function">idᵥ*</span> <span class="agda2-highlight-bound-variable">n</span> <span class="agda2-highlight-bound-variable">m</span> <span class="agda2-highlight-bound-variable">xs</span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-bound-variable">xs</span>
</pre>
<p>and none of</p>
<pre> <span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-function">idᵥ*</span> <span class="agda2-highlight-number">2</span> <span class="agda2-highlight-symbol"><span class="agda2-highlight-unsolved-meta">_</span></span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-unsolved-constraint"><span class="agda2-highlight-unsolved-meta"><span class="agda2-highlight-number">1</span></span></span><span class="agda2-highlight-unsolved-constraint"><span class="agda2-highlight-unsolved-meta"> </span></span><span class="agda2-highlight-operator"><span class="agda2-highlight-inductive-constructor"><span class="agda2-highlight-unsolved-meta"><span class="agda2-highlight-unsolved-constraint">∷ᵥ</span></span></span></span><span class="agda2-highlight-unsolved-constraint"><span class="agda2-highlight-unsolved-meta"> </span></span><span class="agda2-highlight-unsolved-constraint"><span class="agda2-highlight-unsolved-meta"><span class="agda2-highlight-number">2</span></span></span><span class="agda2-highlight-unsolved-constraint"><span class="agda2-highlight-unsolved-meta"> </span></span><span class="agda2-highlight-operator"><span class="agda2-highlight-inductive-constructor"><span class="agda2-highlight-unsolved-meta"><span class="agda2-highlight-unsolved-constraint">∷ᵥ</span></span></span></span><span class="agda2-highlight-unsolved-constraint"><span class="agda2-highlight-unsolved-meta"> </span></span><span class="agda2-highlight-unsolved-constraint"><span class="agda2-highlight-unsolved-meta"><span class="agda2-highlight-inductive-constructor">[]ᵥ</span></span></span><span class="agda2-highlight-symbol">)</span> <span class="comment">-- `m` can't be inferred</span>
<span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-function">idᵥ*</span> <span class="agda2-highlight-symbol">_</span> <span class="agda2-highlight-number">1</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-number">1</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-inductive-constructor">∷ᵥ</span></span> <span class="agda2-highlight-number"><span class="agda2-highlight-unsolved-meta">2</span></span><span class="agda2-highlight-unsolved-meta"> </span><span class="agda2-highlight-operator"><span class="agda2-highlight-inductive-constructor"><span class="agda2-highlight-unsolved-meta">∷ᵥ</span></span></span><span class="agda2-highlight-unsolved-meta"> </span><span class="agda2-highlight-unsolved-constraint"><span class="agda2-highlight-unsolved-meta"><span class="agda2-highlight-inductive-constructor">[]ᵥ</span></span></span><span class="agda2-highlight-symbol">)</span> <span class="comment">-- `n` can't be inferred</span>
</pre>
<p>type check, unlike</p>
<pre> <span class="agda2-highlight-symbol"><span class="agda2-highlight-function">_</span></span> <span class="agda2-highlight-symbol">=</span> <span class="agda2-highlight-function">idᵥ*</span> <span class="agda2-highlight-number">2</span> <span class="agda2-highlight-number">1</span> <span class="agda2-highlight-symbol">(</span><span class="agda2-highlight-number">1</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-inductive-constructor">∷ᵥ</span></span> <span class="agda2-highlight-number">2</span> <span class="agda2-highlight-operator"><span class="agda2-highlight-inductive-constructor">∷ᵥ</span></span> <span class="agda2-highlight-inductive-constructor">[]ᵥ</span><span class="agda2-highlight-symbol">)</span>
</pre>
<h4 id="example-4-__-two-arguments">Example 4: <code>_+′_</code>, two arguments</h4>
<p>With this definition:</p>