From 2b2aa228e301998da82793386ac5d59c983c218c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 8 Jan 2014 12:34:55 -0800
Subject: [PATCH] refactor(builtin/kernel): start with small universes

The universe constraint manager is more flexible now.
We don't need to start with a huge universe  U >= 512.
We can start small, and increase it on demand.

If module mod1 needs it, it can always add

   universe U >= 3

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/builtin/kernel.lean                     |   4 +---
 src/builtin/obj/kernel.olean                | Bin 15086 -> 15032 bytes
 src/kernel/builtin.cpp                      |   2 --
 src/kernel/builtin.h                        |   1 -
 src/library/elaborator/elaborator.cpp       |  16 +++-------------
 src/tests/library/elaborator/elaborator.cpp |   6 ++++--
 tests/lean/cast4.lean                       |   3 +++
 tests/lean/cast4.lean.expected.out          |   1 +
 tests/lean/norm_bug1.lean                   |   3 +++
 tests/lean/norm_bug1.lean.expected.out      |   1 +
 tests/lean/tst15.lean                       |   2 ++
 tests/lean/tst5.lean                        |   1 +
 tests/lean/type_inf_bug1.lean               |   3 +++
 tests/lean/type_inf_bug1.lean.expected.out  |   1 +
 tests/lean/univ.lean                        |   3 +++
 tests/lean/univ.lean.expected.out           |   5 +++--
 tests/lean/univ2.lean                       |   4 +++-
 tests/lean/univ2.lean.expected.out          |   3 +--
 18 files changed, 33 insertions(+), 26 deletions(-)

diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean
index 68240a21a..ba17645ca 100644
--- a/src/builtin/kernel.lean
+++ b/src/builtin/kernel.lean
@@ -1,7 +1,6 @@
 import macros
 
-universe M ≥ 512
-universe U ≥ M+512
+universe U ≥ 1
 
 variable Bool : Type
 -- The following builtin declarations can be removed as soon as Lean supports inductive datatypes and match expressions
@@ -10,7 +9,6 @@ builtin false : Bool
 builtin if {A : (Type U)} : Bool → A → A → A
 
 definition TypeU := (Type U)
-definition TypeM := (Type M)
 
 definition not (a : Bool) : Bool
 := a → false
diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean
index 1cd0eb5b84b0324694c10362e699a51ac66a3aca..1729d77efadeadb278fac1fdcdd186afdaa2925e 100644
GIT binary patch
literal 15032
zcmbVT4UnBxdH&A1Ke-5-npB#SL^rT*SVe{=ZkRE3A%Tj!s|8Y{#nw)^+1yPoY<83V
zi2=cu25>E-6<Z}$+Yy`sYH6$eWzgbOtAVkl5>uzNX(gpihlaKqTN*92@AEw0Ip@3I
z-c8h<*|YEYd;j0}{Czt$(P~bPw<lUz{^RB*+xuG6Gp)?OHFM5dt?=8YX0v_G>C9g-
zH8qhfL9=yipKDLdwkNa7?DSkKi?#9QgiVjt_INh3dr#)=FDAJit?|rny=hPDt%fKk
zfSzm#iVC|Yjb7b1Gmj<~S-l3h&H`QH0o_+m%{FJ-Q<La&{?C60f3pG3s%1nsHBD@2
zCxRu!^%B-=emnkVbs+5nbT*j+)YFOjmRqulwZ4L=&&oPG-*JgLF>iTi*RlBr3w`9M
zIk^J^vvX=j6+iXJhj;)t_~}8hlylm<_e``~Gic~GuVY4u^R;WqKp#1OX^Hbo-l0z5
zU0LS*fkGd-Xzg#$%+8oTH_I?p1FwzhZ2*akL>;e2eHFo%16&=X+mBk-qbf^E+7OMs
z#E%iHf>@1uZYYkEH=NHA#C`$520>vXC&CH$!_OM~b*@vwAv)4}DrSwmWwNywqq7TZ
zCL?}U1tT?rk#fG#IS{b-TcwQs*n2--z~7%W_h){rY0&|l;b%$R53iHkkzr@`^{SJ1
zAH=WsIU8QVoCdH=x5g*BD2Yf^1imh@Db8We%-r@F#8oa;K%F!jED2K7hy_IldqZT8
z_y@tt5OqBSa4^tYZ<VUEADWUhrT#abMxV7@AD7iY5I>h21XNkJNwK`1nyi7hDw+pt
zUQRTE+6EMz=H6&672^Y<w`Q9~!LP7N6EiZ(Voo-0ExAvkxz|jsDuwIi&>-OzR`bML
zwX8OtwI^q%ry@qv*>(&^M#*JaLA3>v<dW*!6fllPjJ{d25r}2kTfiZHw$}a5$ZA3T
zX2jvxK1ivyVSFz^3egj&!S!e%Xa@B5v~6niib(OwC=*#WEhQ4f*fgrr62;ljQQH>C
zU1#Ki9d^y!w0rkLVlm2lg7OR)2LIUr1t0@M0V7No1=uw^-JDcH!gxa^0Svej4Jn0~
z_sTK`jIj&;EO#3-NbWX9g0M&y3GTE?9X{>c?5@nuPPg~9n-fIgUg_}{QI=;u4rxJ3
zxmf*`=vt1V!FV~FAam6;!1`LEcy$(hjtTU3HY#-HIm1X-y;j%OM7uyB=!!FXh<G0n
z6MQE?zZT`49TX_2P@}U4qM19)P47s&M+L#bq@bl3?1}njfXc=10;mLh3&5oml_a9$
z-DK_3U~8}C<fx!vmlQDrks2Lsh}7N<yrTAt3H&910~~N0z@Y(@!zidnB`Q?khoY0C
zTdl=HxpPf;{VmLXJE+cEORMFvdwyBHKz1)p(l%Lw6Xqr_NF+~7q8*H)8KmKKwn2(;
zC(ug9_atyWf$s%)kYj&EpdZe$P~(i07<+fv5X2t%v}9$B+T!-Z@JcD}BiRpttXRA|
zfgeoZuK^T`zYcKBQhClIz3^T%N@hTv9RI4dB#w>SA56RC^AqIrH-KDxek6e(P2k4>
zf;sv1!NjICnV97gqm+O-jgW{AS|u?%X}ebZ8q>kD^+LoS;8e19AHX{CcZTF4bkN!?
z8nRnN+%@XIf;o!%2LMXs2LXOXB2XM=9mZ~t_JK4*Y0bRfCMiO9YX=T2i>_$sRGbsJ
zJor<bLNPy`K<>&{u=OEMi^?ACXPhB7*rJYt3s+1UpR^VWQ6#6aDO+iqd#1Dp{@buE
zOM7QS3Iy2-117f<T&m;>EIE2DhNwn6{+?AtqZ%?`Il~HD3S%r#`A&_(7xL5}1GlX3
zCkgyhfHKp=0FP_om;;;*^`m?W1y#V9i0u85HHR36FEEbH7qA0VV0D;ivbjA!$pGI9
z6iT3<2Pnq=EP;;#JSlEqe;a+4-__jL+Sb~?XF7AqdyYe`B6wU32l`}s@GMOJf<t*K
z*;fXD48^E#peivF6yoZ0)|A_$>WdN=4swMQE2EzTo~3j#hJ*w?gjRu%0X%7p$(B7y
z=cl@Jj`3nK?@y{YmHGnHU$&;)QKwroQxp4I>$=-#U6ytPNdx~%&i@j4#qM7v@CgIm
zGUHsC>Nt9O1KqD$B|5L2E6=zcmFogW4;fhrkQS7i97bI{d_93j0Lp*=Mj*F?atF>n
zk`&51WxG7E`J_!MvWWm&#DS$BvX%5B-u@1x#oON}@Th^VUx@_1V=jz>*)B#AqN~in
zY5d7i8VUSOU=!7+6L`!(*H0BbkJcVB06*x;z&~1ZV8E^<Xr~Sh$d7HOl_#6zCKN}z
ztA7S|@$xSK)k>GJM3`@9kFQ17cTpr$2uZNVGuEf1;sZ0#M$B_EED|2D<gT)uAPSk|
z-vEl46A63{U{7R5i%y{Xto0?ji>BEz;K<KVB|XT0J5moe@~`C#2Bub`ZxI8->e~rq
znh?w1u~s+C0sjSXgdlBsDw)*|no>c*zefuRW0YB;r_eH@l=oGhSnD7?f+FO{m_^(c
znh7rDwqV4lk)qyJ-GH`6w<0L>Kdm$0fZ$4CZWdPy1<QrX0U+@x<j~&(C?))_L2gWE
zY@o9tD2h9Uy=W*HR6&{SOI^|abg`J3;D1`V%f~*kNYQ4Ybmu^U7e$V2rmL2q{eb}t
zp(W_jBqeD!qeq8cq8ubcx3LvPhvSn{&{^0D6GJ*F#t@{W?;?k^qc~gwq>MX9dgkhK
z*P*DBw5=RVe9H^S5j~AmM~H%5LPq4dfgQ&2sC#wCE$6Yj=F=I)2Jsv+*~%8ta|mmm
zs{27;9SW%sP$M-K@&$;yA3?w5eknl7y$m3=?~oImZDTF<5X)=ORluU~U`SB+`7VIO
zIV@yo2cJvZY1>AdL}#>6=UKkQfh6QsElHR*^4bDW7c_u+C^olE68py?ki<R@pv30#
z#4PAmS)=<9r>zF~;cg}$MSmufM_v@?w7XP+gy7zXk%=McGI+#~Ssy(jKO3})N4iD*
zxQmu3HgT7=L<<(Q1fK4pcxw#Io#A|d(#iz@r4<@mT0s!H2RRM$x=(h~ik6YCT3IY4
zdJS1rfN$-!1J{Cc5jD!f+31`%(r40huL464GyC3)0UDK*&tPZpvxk`Gg9R?c1RkkL
zeZhWf7#On#CkY3YK&^`W#T=kjf_hfYbuoQ#+PqcQ6PMTv^e?hDrByo+?VQFgb2Ep<
zyRXjcLiAl9R)WE>ppWTjD(8~fFi>WsZ^-+}!CNQ+SJ<rtIqiCaT&1|;x=Vo}UrRO`
zTl-PZMu<I`Q$APoyU^*rE<TdGU9RlSNo<8O++!FVGsRC>CHMf2g*&I$chy1@vocG2
z+Sb@MVVo^Dmb5^950WH7dGJPzl@@*yptSIMfKn3!M`JHT>y1>%<p7!X-ID+*c@R2R
ziG=2S%DAm8G{(E9F+B?XI;(UF-Bo5u$cti3FIrw&7&YN(;A|5!BSz)k5LtCcD9RP+
zlLoE?C=L7+K>5KN0Ll-p0w_OtBS0oR$6(k*WJEspYLCvHJfSN6QSSnw5RU=wzmwCT
z(H-Fq#l4Q9ss}tcy{}=MZX+3R(zCTm?F~(Xzi5=_;!ReP%Z1AZ2b6W*^XBob*RDLl
zpx4w99&c8Mt7hE_=md?mAgrv^?t;Kmyl@oN@@9b2@lOL>&DN^{DqCD*kUy8L*8*H2
zO5EMsKHUEdhGxh6Q9c#ODd=!D;SO`^R&<Z7MG3cZJmq1-i57R5{zv680H{laLP$Gr
zvT<Q`_W3hl$bAbn(*#;X9`R?r!0%s%Hd%-~U5C0ve>*^l{&N5oU_TGAmuWF%6GbTm
z%Qi@4dWx{3m0X8or~6rJDIB`SruhCK?$WIZ#C6N4gXO>>@yX-$sLK$X#cMnFMQe1+
ztneFy3YQI_jnT)r1|M#d6}C!-fE&^g@maLyiU5QG%(LMP`3zd~eJh}F2Jssc5n0DN
z6=R7AcQu{~iHuM+i3IPOv|^|S1ctbSw1Z%CW@c*4@=94lVFOWbL@niXW1alkH3e9@
z0Z65_8xuG|5I#r+`fKWFI0waX`?a%}+{IrbF%#;7dDEODHpjmWv!n3-ZAn3l??DZx
zkI-pG6H*Nb^Cj^pd`jA3l4zj%cH>LAbCBK8t*6J1q~XMd;k4Em05hi*G==!Y7=Kle
z^4i2J<a5I%UNwg{gn(jD9Bc+6aNvKz3S<GLbT{0IGaD-7B-_y?ic)P(no)j?%<Hy3
z>Z2f_oQb{$oSqiuwKZ=Q3NJ~?ZxmhBl=hD|L4*`n{$|u6G5-3SlSFj+Q~-r*v&aYQ
zAS3f}9I4=Cs|tSjcviS_Df7goNj$w9v<o~PKt1wwpu`g=MuM(w>?oc+b$SAmqa9J{
z&ZzHTv~W39U{pL3Ma@cgJHR^mxr3k;{{1M#G8YTC4PCkcXz=>q-O83|DtyD!T{8{?
zsYjkh-Fr~43++W&U-3!N-@~zMQQm34{-c2AW6?payLcjm8KQO<z_NHBw>Hso(67JS
zikw9W2jbQe)H&Onn=QQ1lLqxB8qk(WWQG3-z}t~6+)jW(fzNeLw{qwba3v?8(Beg|
zlmkDA*5pmRTl5d*PV4%05_l4Ww0!031a1s-$B}bs`FN__975$GXx@J&O=1Lp7In^-
z3$pPKON~?&<ZLg9*(4Vgr}&_ylSKYe;EVC`Xo-fnk3pK)WQTf*AhPj&u0tzfwTv86
zIHBrnbp16O<35IwGRJQw@V5wpAuUOd8RQ=i3Vkeb%Jg<9$;A|^^aowK^MFX?(<Jf4
zNwk6{fy5KBu{bl(eLSMbdt*J{HFWaf4}mx@aXgsGZ+0RHPAU!}Gf`pw8&T~@0}BE(
zIe>CO%_z7}fKI^yo<==7z|)CA>Lj12l%6$`IE7vynD5|ZK|&%YDIv)fAH>9Rig?!A
zym(To`T$1p^kAQ1Ac?yB*pec=`|6N{XXfQm!+jc43&QhK*$3;LOp2#?O4-5t^Ccnq
zXkkp0p1gE7gs_1D@$&oRWxz^z2SN0_fI?g`uRVtz&6Mz;LPH_Fl|TH@ij#!rVj_Zn
zfSF173f#eXk!>qA2(PD1?SANxlo9uPxtFG#q{h=LM`NfQyaw`n)56O-9fHEieK1Df
z$rJ{$pCi*C<hzAi-83nG-B}L4$-@E2>OP0MGRfx&!kr5r*CYh~A)1*8sKKRSDEB;B
z;rjspY#ds_!6M`Mc|a@}Ga#~X<_l@&k9M1hHtvD+m<p-OS7zHWhR-edTRAsk<i=dj
zs_si1Llyi*0>8`&l<VF;G-I31WK+3Fq4x+{^PB`I-e`Q$D&cSjquCbiwC2zWjZRrG
z2U2!!j>icG9qX>8sN;>4iwMqSj(g(JAJiQ0Pcy$CbC}R)u*RhkVbL02OJYBnz{3Vs
zE-hJuC$-9(WsO4^+|3$)ZOuh%;M>M7=D_TW8z}S8HOTQvSRwHZbTK_F3<*wS(ZiBP
z=n3}f^lT1Lt_LV9uyGy~SS%709HndrutGDik+WE^T8IirdwM(MQsbnW@9_Qsprqzj
zP2e}tdU44F*_bs}rep#fT)Ud!s5N((Aphoj5i^`jj===0^z=_aE>@l)81&m24*@3?
zF_bW|zDS-5b7+>r*8{B6nA9zcMQj6(?n=~XrSeRSDViqN!Wqm{&<3|Q{1(J<<&!r4
z9e4%)2f&kM8y&R9%H6WjF^uRICOFI$ZN%&6E`buRzVrnvy+#~;8;Hfm$pn4}ARjq>
zHMZ)#sLnbH%0*N2E+Zz=Z&_c?Q`H_NvaZ*2wZg^a7GTTz1CKXwxzF$C!ikQX)eSIJ
zw~lRG2mS|WY6MRK)D7Nu0czL%J%Be1SmCRb;}vKiYN~(|R(=<a=&t-WiU<0v%!yt|
z55dJJE>=)(CWxXi1J$UG=dBX2D!Ch&nr=>DH_5qK(nMOSv#m)|d(c&^P}OTdm0U<t
zPj6ohnbMA{@-TSL&JNd<g?|xPW9^kkcyx0xl--@9<qJCXUB?!l7$q5L_9jVDuRIz#
zT5DCk5K?-cyLw3*`CAvQ*=+#X{|I(XTKC7LgglDMn#f(D@^Dgv-6}~9`p}#%N3;6|
z@YC%6EPyn-e~Cer{8dfbK;QLf{hEU6|IkqI;$Sh}$`^yG@NXuVvA|%7Nvh{d7<4}E
z#6?N0@#(s3r=y9p3pfj?3JOy{b$Nc$UCz%LbaymZA8}fFg8Xpp5kD^jC8_FM3^)o~
zX8EQmNtD!%?rrv4(Z_<GuF*|>*kA_r<*d$4j!#YO=y)7d5ZSXu6NuyGeB}gH037b|
z#76uF3w=(pvLAESp%_I$7hpcxKsmXo;$6O9g?`D2_i!zi{^bT$PB5I^o6yWGpnzu@
zvBTp#)o!N&63R9($i_+fHRu~bK{cdzfXa)B|K}3_{F=uz-HdQRl0c75lmN20!|(}S
z_*7mr+Ll1=r}84m`pxtg(j5gi*|7Zz0i{px`fdx+Y{4MnCZ8#@x-EG;xh*Ar3h!4S
zR9#|BOt!M5@q*Z7>N1Q1`l|kUfX^J_s(Ow!XG3r;|CxxP$S`^;7$he1_Z@#8+QYlH
z-o4~Q>to(5K7AE@D5}5s%#*yhB&?EuQV<>d{u-z=9^^w8f<gJv06->4|0;v3eQ4lA
zi^G1u!fb!PLA-vT<2YWRRF|PK87R}IS|#_zoyB?#tUM2*l@|cp!<bT^o(q!e<j;y2
zgGH=50O_<;0dEx?f)9Bz-q#3KxgR7$G(}bN)0m$vS&42VR+HUhrsR}vW;&gfNPz)V
zH})#n!c_ZeR(eV<mA}^Nxyrddb6?I|u`nS&;-BEkMTaQ_aenz_5(7`QPlHG~MS4Cc
k_#BMo+%<dbUp@1*r3%(;L3TP4fK#h`!{m;u@ZYNc59NgT;s5{u

literal 15086
zcmbVT4UnBxdH&A1_ik=hWuu``Y7*VV&4#s@NyH5^MmIldm+XQ-3S%oB=kDe%x#MOx
z+1<o2#-cL85bJ2gs!+8~gCioAw*K^oK^tbY3XCn47@g9l1WTI^4Q(~HG+O#T&-0yg
zzWeRnM7=XP`<}n||9#Kjm+8r7V``!`+062v+dI|T*PNMcX8x+oxh(UU%lz2%T$Vbn
zj~$$}uQ8MPEz{GJ*&-WnKR33wH96Os$|`d+dz)FTO*AGAZ>+W^vMYD(&b<A_B)6kE
zk@;W0d3W=ALj+7LjDtn!uf^`GLN}V#>Df7DTz2_}v24EzimYB^$pT$s(5n9G>AA*S
zYkCS@&OdY?{$^`9bx}ri(=)_|_Bx8i#PvefYkmxWvpSHj0`wws45+6a^??KAWd%{c
zAZzcuajiNr@51)3lZWmp^pT^+)D8^HE~pt*{OXYp@c?e{>p`)Eb6UH0Pqvz~Xy`Pr
zZAOXn)vL+CDsujk66b4gR44E*D|7zYLLa$k?r+V`&6++p%Q`g!uZimI1`_I6_F94Z
za;p1f09OR*_M?{dsLGO(c8kUy;>U>PL9Fhs+)x}R?3^d;ufX7L66yokLnee1zKP#T
z`{!J{gs-C`t*2sE%3G$IdpP{kn#qXY@?fOyV5FRHbPfdU{Z=VsKY9D73;6r9#{SHY
zH!O6ZGyE2J`QdePJF3oEeZA`B-3RgOtKgLt%;^S}ndZb~2PIKzV(Jcjt+Of4Vb1K{
zv021bE>%FCG#e}lQq+hAMH_oVWRFA!!O9RVFa&Tg(7W6!RcAk%k~F3ME6<_NTCR^x
zH4wyavq9?#ZBZ;=PEFRpTNUktH7_R`L2Uzyc5`pEmWuHK(VKIPqTpMs(!h+2x-uu5
zu$J5>(cEkCs49i)<<KDE8?5Guw`wVGB5O^}%}hs(rn4~&M@GqIxrAy9B*`V!w<Ta4
zjTn8SWTP#_bv-!5?}jdaQ)IQEely~5Y#*eBC}1x^3egj&U1xY`A!r8lcDHQmX5u$h
zM2cIZOk~-*5(#1)HxZ>JinF1u)(GT&(+~$c?3}%M*RJ`*VwCp;<ry$ch6X4A85jx}
z$BP2&oSSJ(DIsA(6u^M3#1N62_sTK`0EPLlQIWef4U)SxNe~vvBEgnby5Q5!&F#$m
z+)Qg<t1*conR|uDA7SBC4rxM4xmcaK=|YU^X1u(JAam6m!1`*U_|+`<9MRmy#u*IA
z4x{Kc(p9gew>jA=5D2>Bj2<GUS(GJj#$>-5<)JnT^nIa5XAeX(ci20#Bk>*;1P7CX
zmSC_al>-1p<y`=kfPWj{5{gO^(ed7C?b2X#kLBd3pkS92F$0kr9c_rz-VMB>_MQa3
z7vKN~+zN1L4a#jOs7EC#R6mHKougZ<#X`A#P1tyV*>4Bcc}r=vJo&Nrsu#$P&?GIB
zB{*Sj@`6P2v?SVHQ8a@zoX$2#5e@;ZWV}6rG?H51kJh_5_ICvO;T#J!&Pa)|_dXkf
z*aM%Itc+1x+<p;Wo1k?!$$l81n7Jc?A4%Zv0ThcL1=zGyp0h|VJc35a45*#s-?f&+
zv2pwJX_tI{hJ5}$kc-bxB=D07{1iYiC%?Wcu_;X^X1T<WW4dEpTkkRiiP<UJwc?*K
z9V}a~6BQ%=Ajl~~?gm)z5Rwn0gVtujkgxiPxMS3R3v(3pp93h7?*;fRiI8|;?Dl9M
zNHdhy%zJE-B6OE_;J{+OJBGjWRy4FJ&MBZg_&$!L1-_8LKLU6OTki+BBr1Ebk8y_F
zV2e5m`btb1pSKnZQ6#7FX<KO<yQj4W{`;^kOM7QS3Is;T4^N5bB}%TqlB1^y>2%SK
ze`0;2Q4JZeoMFovzyg);)F^x*PyIPa$qIjwz`q12Gd%$ClopP60M3T`P(FczDrjf#
z&#XDbFnob=Y`%aUpaQGSL{p8i{3HW>m!MDr{Te_q_E!l!3h<1$f&FdtV!yMoulcs-
z{@pW~OWtz|Y8Am#VmQzz(}RmK`5}k$Y_hKm02zu=-;JuoOwg72PW`Lal-onzA0#du
z<cdxS4A~hJOXy+@2?_czS_M7=@Qg7gTlOTKpY6;!#*4+gKdItu>I+PN)0%QeooUWa
zPws23>ujHOS=tdK4g4E9{~O>HyMLR&#|(5!jdNwHQ|RdpbiZwt=)88WJnwc?t_vJJ
zWMmmYT2O9s40ZAF-2@&7DF6MQKyC-+4xD{FDU@}}wmGo*xJ@dui2z%`fu$d^mGmRt
z{sE-L+dn4ogn_PKi3Gl5E{uZNE(STGtIWVT{K?@!mkWFnpr}5Tz#kas`l-U_(Apyg
z;0GNUc+#2!19l}rJGE&*$t#}63L8g?qqXB-fL*-&D?qi<B`gu<+u2i0{69f|GKG)?
zdpvD@N-91u18u}SC&Oaj0xY?!a2HFP$Q=KUE-`aDfzJZ$iOgux33Q*azC?GyG&>F)
z`HGXmg(Ap*+folU@~`F$2Bub`9})w@>PHD=nh?uBwpO=|1O6M}2tnHNY%;4IG^K)q
ze~%Ut#wfEwPoZT*Dev1nv37wpHxMB|#w_Bt(@bzFw;jVqjTH5+>ISqiQI?CK%>S|h
z`33}60(<9hwNS8Js2l_)k3tdrQ-D&!{~6?(I%5N!4M9=dDQLY-231fd`%+i5KkXAU
z6Z}srclp>S7Ae&}DBV>+lUF&e3NT%@1nm#3LHjlobZNN)Ew+`7b(BOoNQQ1@D~dM9
zcThvnS=b71#;}Dho8CnZiC!Gi)QmevdZw9iA{dG~N!!Y1;#*#Tk%}JjJwn9n5;F9M
zq~#V_g=h7v+ip2ezW-1<qu3yxL#CS90(uT%%~N$B2ryWrLR7m`V<BHq?iZt9a=(N_
z*}4=UeaRswI6GNd>LHd_p{syp73w_<3F<!I1&}z0MPcD{X*+G(Xp`u?7HU7smpG7w
z+^VsMVyBI~wg7CT0n|eQxowizzXAbd?w10T*j%1yN4MM>-N!g>1;CGYGWjU_GnqW{
zqBxh+qPrUj!F>>5Vo18oL*D(e_0c1ArZW{4j&uw9aR)6?Y~n6!i54tq2|V3N@m7K}
zX@zE$Rv2#53MG?PD9XK@hNaYfzLQppfl$)QLLt#>$f5##bB`Uk=ADZeQ&g)1$Kq`O
zAd{YZr9tiiX5S-d)u^O=&S#oq4>27M7Pu4>c%&xvdHbzlV9dG;IH&|_Rpi%lfL00W
zSvl9m^g+^xt*Q;5*bDS8v)M|kb|AWG2D{A7K$z~n+OG@IH5OKa!LXn=bu^W8(U@`r
z@=D*3oiE4q>)HAmfHx52v@wEQrMTj{D=;8mOEwx?`%%wEh&`E8K3DTQ(doV`K9aj_
zR`%v3wn7>15e$x*0%{39fMelJGwVBQp@CVMr9EwHY@0B_mR%(+P~U?jNl+fV5o4u=
z*8!9kUJp<nMU83fCbaINLTC)8efKz8DR~e&SBZq?e9G7;3ytyaDNK(-zt$@4LU)u|
z67r%L(~Fju7Di3@b?C~rFf#(my&<ydj#HF3pidfjBS2~3O#tNwzXni#K)074T!~gD
zJhu(t79u0^<^a~;ti=<m(jWCM5DM{CE8PDir$M7T&K-(-Ekkt?@G+PAMHr{ILq@6e
zjBb+a)-;9@M|m#Z>`N{eE*sodo7csA-aNkb+Lb4m7-iQ0f3_mrmFsd(Cupn%`HrKs
zPYo`oc;P6j<!XS^@tXmzU@J)|TU=|6{$jRX2k;V6;_lvd5+03qpU{W$i4f-sI$TY-
zW1M;ex<`=WGPsrFDGwV?w76sRKPry_KwT;nLfW~?#)Z|{=g)v4_s!Q#j6CAcdV$|x
z1X{8XdBW2`F8W&mO7t56D!_gVU@y~R$R>(X2$pS-$n+FpMJu@u$4>Vf)>1fhjZgFa
zLENQVle&#^OQ{2FXYyNO^2nHxA;!_gYdiOKgWOUp{KlZdrEAc((+X`k!H3&|s%>WT
zfE&^g@foxhwy_vM7Y%2~r#XP>L0+8`@f#BnS;qz{#u5?kYWyakAO@-?k>FjE-bU2J
zf!smbL9j79J3VfBrL3W_fvBfbX-+q3je)w9TAKt?X>C^mrwGCasX%{i7aA@=amxPL
zSxoNeua%eyb-}!8&T*UL--6juc>k89AjbEghSNvrG@}Wr288*NcoaS*?I?ku`c~sh
zxpR=+o7iYYHj;)DTeKE^#mtG3n^2HXjPb)k%IgxZkk4%^@v1rU0-GZS#lcn}Ld^KL
zS%EAd4|ChvaoQ6X`Y(v`bCO&SN-IjWHEBlqF*2{)`lt`Qy$(x2InyT4fC!!z)=L#`
z6$&p&$#05B+L}#r@5J;JSN;I%;0}NNfg}-KJ{3^5dpnDKunsaZAIB+=1?T4DS>ej1
z%##N}?P=c)u)xzn)FV#^OFVI6B<S95>?oc+b$S|;qa9J{%&2c;v~W39U{pL31(kOj
zz&iPPA3-bphfs)RE*4I{qq)5Pceh}0{-|iC!UsN`HRCuAg(Jb+0oH}~vTRlHNzvbl
zJ|1GSLk9UzqJB6Q(J?@+vv@QZNs8JBFu5$=A6lDeIq28lfkB!n;Xu47Tx0KC;f21A
zPU=lGpe>Wg3jYa!w;@_w3!pg0=Q`(FIdloQj1y33@gi5sfgeF@@+RIb`ulUIb^SUC
zaI>i8D_<v`#I&@UnA6aLPn4TOsNBEWdi)pDq(0QYggTv5F385Olp5)IkaK>_Cb_6$
z#Rn~&B=SdrFUH5w5)Fk$4AR6VJ7VAz)crHAL(3Rn<dDJ%RePiBr{8`G9LgMjkibt9
z1VdVq9x=#28Wj3S;*{y_;UpL8dbjb=rF$vrBA+ISCr+XjG|2|~$6{k~W}y3MM3MK#
zdcJFD=fgh?;=IHmGr7w|63WemL1ZQ>%zr;xzhht~2T(4k88P=6kSsXBQ>aG=cq%bS
zo#Yeqn^a~9`DvjS2oAS#GA|*K6X6m$E8V>S%PHa+YxCkssp`WRrGtLAlEmF?NfF+8
zbx6W9_B@6E0;U#(=cTd_);mMtQ`jl(2Jg?8gyf@CfyPAX$;-S9NnSJ(42YLMB`>7~
z;CXb5D-iO}VvuG^`1{aMjJMK<A6jve@CPwm1iuV0317h-rFF@+l|>L<Pnp{NAUYHn
zO907BlXBE}ZslkUm4o+BevDdpS*Jr#IJpnT=sTIhAog=)8iaf|f2*4&<*z#zf^YJ0
zkk<by>dGWvBZ%lMd|Z<d`1@&QBA^DBgrPTMN>=zjz&{g*R&cP$IQ}po7Wt}L^Ydpu
zpJx72r<rKO*FE+L2vh^9%U5P&7{lil{H<IZF>+(BXI1wNj-d+vI)UHh1j=;;3ulIH
zHZxM?GKJoQXe};d;Yj&)jLfgnz?tns&S?&v(CCx}b0B5s=6IA~(6R1XiaOp%xrpF=
z=D0Hs{dvvtp)~VnF^36#9&20?5f-iSoh0_-2|Q+C<%*Iucv7oeEo*QY=wyw*v#CXE
z;M>Ly<^Zj=+(PA{YjyWMv??UNPq4EMIISB4^noso&=bbCdp5@^*8`LlIG6FjVu7IG
zRAoC(r5Vao$wi6^NPBKO<Wl3Ln(y%b3818YGJz)nt}U4$Yg%Jvk4%7rYsY{%Va;tO
z$iMkszzk=SV{j2sdirM|7gtXc4Ek-4hk%oM8A_N~Um#C~IW$Y*>jBnjOqzwo0=5B1
zA4t?_rSeRSDI}~`u7&fMr=SgPZTKyS<H{#({0Hy~{7-;q$~NNnTzAMuKfs7iVS>Y4
z(MG&}?hq*9zE5AU(rd)gkAPTgoJru10rHX4cg0q{7tx(rP%fI9cNy_&_=h$l=c#Is
z5?ROVxmx(@+%7J0r<i5^fyYUmel9{|{IHsv)eSIJesLF$dhBS_ti$~;X4D9t1*jXm
zp8(XZ`=<aW*I41ZDA&u;Knzp?C9M208X2meHK6i2tRp$metO7t7+|cS+)5BdVFs#E
z9nV=MUR828Fg??l#BOpk#$`zpX{pX`NRrxvu409%UJ0t6Y*12P0ge@r$;Bgg<pHgI
z;hM7WUj$a#z{-O>x;Yri?#|KjkWPKP164keWTe@fBt^Y)G;#!=)e9k|KWf#im$Z?;
zb<vvL3XuH|rVKYBCFD_5)<o_Kl?Rd<>{dx?(1+%9Ihx%wM@Shj04bW?ztEsc{;DQz
zpl=MV-(gUB=7|nL#asDeP!;~032@9aSYndu`3459qMf)XiM1D_wQQ#oi8CO{R<TS9
zQ$KaND(Nog=RCSQ5v-3mtvp74xb}#ji$G7Rx)=jaz?Rt&F_a`qYDag&{#Ep`pr>ne
zQXe*$L47%^d#5I*CwH_x4qgL%c(wpe%do-Zr>O$qaE~T7QXXLUvOdgtHHuLbbOGk0
z4V06cDn4WQ<>;53cn_Cz`<EG1In8i(SD~3%pu&J>8nMIUJJfEcfpvs7Fvxb2^sCS^
zf`V#D?*P^GJ)L_t@jpVgUXBSPB?<J{L<t~^I|dW*!l!B<;SXB^wO=&@S-+L$A>C1M
z!%t9zfYPUTeYc%xwqp=+lh5wRk=vffliOb6r|^CSLe<5_ggxw2Y-+q9HksOlQ9xhS
ze;(j7hdv^zUSQ4H5M0ZDF=8k(jGh_>iOGC3?s0+9(TCQ@ylMZHqLU9%8n{pKnJ0O1
zNmwQSq#!!@Jz&UFzw)6=flfX&0FYN|{*?w*`{Wb`I_&o=%=Y&f#Ont-j^hPNbtxK?
zfiiunRdQe4S**vv%5(iFp9gFYV@iFaW$tMTa*su<I)HvHRlr*Xhu}k=jQ2G{RqhAL
z5KU2){50m5N>-xVh}C5Gu(o;d*wIYqvJxpUfa*5Af-Ow7k1D_1Ks~|v*8r5txju7W
z&RelCAwS}u=E_BfDFktT`DGFVPqj~j!0!A(!RO%I&b@iJ{a4RCZK;AaTacZO1mM)_
N-Z-`6P53{q{||(63zPr=

diff --git a/src/kernel/builtin.cpp b/src/kernel/builtin.cpp
index 0e79d06f1..0e6bdf9fb 100644
--- a/src/kernel/builtin.cpp
+++ b/src/kernel/builtin.cpp
@@ -13,9 +13,7 @@ Author: Leonardo de Moura
 namespace lean {
 // =======================================
 // Bultin universe variables m and u
-static level m_lvl(name("M"));
 static level u_lvl(name("U"));
-expr const TypeM = Type(m_lvl);
 expr const TypeU = Type(u_lvl);
 // =======================================
 
diff --git a/src/kernel/builtin.h b/src/kernel/builtin.h
index 2a980ecfc..e5a7e925b 100644
--- a/src/kernel/builtin.h
+++ b/src/kernel/builtin.h
@@ -9,7 +9,6 @@ Author: Leonardo de Moura
 
 namespace lean {
 // See src/builtin/kernel.lean for signatures.
-extern expr const TypeM;
 extern expr const TypeU;
 
 /** \brief Return the Lean Boolean type. */
diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp
index 3d65fb900..6b9ec8307 100644
--- a/src/library/elaborator/elaborator.cpp
+++ b/src/library/elaborator/elaborator.cpp
@@ -148,7 +148,6 @@ class elaborator::imp {
     justification                            m_conflict;
     bool                                     m_first;
     level                                    m_U; // universe U used for builtin kernel axioms
-    level                                    m_M; // universe M
 
     // options
     bool                                     m_use_justifications;
@@ -1179,19 +1178,15 @@ class elaborator::imp {
             // We approximate and only consider the most useful ones.
             justification new_jst(new destruct_justification(c));
             if (is_bool(a)) {
-                expr choices[5] = { Bool, Type(), Type(level() + 1), TypeM, TypeU };
+                expr choices[5] = { Bool, Type(), Type(level() + 1), TypeU };
                 push_active(mk_choice_constraint(get_context(c), b, 5, choices, new_jst));
                 return true;
             } else if (m_env->is_ge(ty_level(a), m_U)) {
                 expr choices[2] = { a, Type(ty_level(a) + 1) };
                 push_active(mk_choice_constraint(get_context(c), b, 2, choices, new_jst));
                 return true;
-            } else if (m_env->is_ge(ty_level(a), m_M)) {
-                expr choices[3] = { a, Type(ty_level(a) + 1), TypeU };
-                push_active(mk_choice_constraint(get_context(c), b, 3, choices, new_jst));
-                return true;
             } else {
-                expr choices[4] = { a, Type(ty_level(a) + 1), TypeM, TypeU };
+                expr choices[4] = { a, Type(ty_level(a) + 1), TypeU };
                 push_active(mk_choice_constraint(get_context(c), b, 4, choices, new_jst));
                 return true;
             }
@@ -1254,13 +1249,9 @@ class elaborator::imp {
                 push_active(mk_choice_constraint(get_context(c), a, 2, choices, new_jst));
                 return true;
             } else if (b == TypeU) {
-                expr choices[5] = { TypeU, TypeM, Type(level() + 1), Type(), Bool };
+                expr choices[5] = { TypeU, Type(level() + 1), Type(), Bool };
                 push_active(mk_choice_constraint(get_context(c), a, 5, choices, new_jst));
                 return true;
-            } else if (b == TypeM) {
-                expr choices[4] = { TypeM, Type(level() + 1), Type(), Bool };
-                push_active(mk_choice_constraint(get_context(c), a, 4, choices, new_jst));
-                return true;
             } else {
                 level const & lvl = ty_level(b);
                 lean_assert(!lvl.is_bottom());
@@ -1772,7 +1763,6 @@ public:
         m_next_id     = 0;
         m_first       = true;
         m_U           = m_env->get_uvar("U");
-        m_M           = m_env->get_uvar("M");
         // display(std::cout);
     }
 
diff --git a/src/tests/library/elaborator/elaborator.cpp b/src/tests/library/elaborator/elaborator.cpp
index 4ca6365c9..f6693a0db 100644
--- a/src/tests/library/elaborator/elaborator.cpp
+++ b/src/tests/library/elaborator/elaborator.cpp
@@ -14,6 +14,7 @@ Author: Leonardo de Moura
 #include "kernel/builtin.h"
 #include "library/io_state_stream.h"
 #include "library/placeholder.h"
+#include "library/printer.h"
 #include "library/arith/arith.h"
 #include "library/elaborator/elaborator.h"
 #include "frontends/lean/frontend.h"
@@ -821,6 +822,7 @@ void tst26() {
     */
     environment env;
     init_test_frontend(env);
+    env->add_uvar_cnstr("U", level() + 2);
     metavar_env menv;
     buffer<unification_constraint> ucs;
     type_checker checker(env);
@@ -861,7 +863,7 @@ void tst27() {
     expr eq = Const("my_eq");
     env->add_var("my_eq", Pi({A, TypeU}, A >> (A >> Bool)));
     env->add_var("g", Pi({A, TypeU}, A >> A));
-    env->add_var("a", TypeM);
+    env->add_var("a", Type());
     expr m1 = menv->mk_metavar();
     expr m2 = menv->mk_metavar();
     expr m3 = menv->mk_metavar();
@@ -872,7 +874,7 @@ void tst27() {
     metavar_env s = elb.next();
     std::cout << s->instantiate_metavars(F) << "\n";
     lean_assert_eq(s->instantiate_metavars(F),
-                   Fun({f, TypeM >> TypeM}, eq(TypeM, g(TypeM >> TypeM, f)(a), a)));
+                   Fun({f, Type() >> Type()}, eq(Type(), g(Type() >> Type(), f)(a), a)));
 }
 
 int main() {
diff --git a/tests/lean/cast4.lean b/tests/lean/cast4.lean
index 92a2dbc6e..9496058bc 100644
--- a/tests/lean/cast4.lean
+++ b/tests/lean/cast4.lean
@@ -1,5 +1,8 @@
 import cast
 set::option pp::colors false
+universe M >= 1
+universe U >= M + 1
+definition TypeM := (Type M)
 
 check fun (A A': TypeM)
           (B   : A -> TypeM)
diff --git a/tests/lean/cast4.lean.expected.out b/tests/lean/cast4.lean.expected.out
index 3ac2e07f2..a162a3574 100644
--- a/tests/lean/cast4.lean.expected.out
+++ b/tests/lean/cast4.lean.expected.out
@@ -2,6 +2,7 @@
   Set: pp::unicode
   Imported 'cast'
   Set: pp::colors
+  Defined: TypeM
 λ (A A' : TypeM)
   (B : A → TypeM)
   (B' : A' → TypeM)
diff --git a/tests/lean/norm_bug1.lean b/tests/lean/norm_bug1.lean
index 983defd58..c22faac50 100644
--- a/tests/lean/norm_bug1.lean
+++ b/tests/lean/norm_bug1.lean
@@ -1,5 +1,8 @@
 import cast
 set::option pp::colors false
+universe M >= 1
+universe U >= M + 1
+definition TypeM := (Type M)
 
 check fun (A A': TypeM)
           (a   : A)
diff --git a/tests/lean/norm_bug1.lean.expected.out b/tests/lean/norm_bug1.lean.expected.out
index cfbb3104f..05a5fdabc 100644
--- a/tests/lean/norm_bug1.lean.expected.out
+++ b/tests/lean/norm_bug1.lean.expected.out
@@ -2,6 +2,7 @@
   Set: pp::unicode
   Imported 'cast'
   Set: pp::colors
+  Defined: TypeM
 λ (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), let b' : A := cast L2 b, L3 : b == b' := cast::eq L2 b in L3 :
     ∀ (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), b == cast L2 b
 λ (A A' : TypeM)
diff --git a/tests/lean/tst15.lean b/tests/lean/tst15.lean
index 5e0956c62..b1116ed13 100644
--- a/tests/lean/tst15.lean
+++ b/tests/lean/tst15.lean
@@ -1,3 +1,5 @@
+universe M >= 1
+universe U >= M + 1
 variable x : (Type max U+1+2 M+1 M+2 3)
 check x
 variable f : (Type U+10) -> Type
diff --git a/tests/lean/tst5.lean b/tests/lean/tst5.lean
index ccdba11e0..0f1b6fa5c 100644
--- a/tests/lean/tst5.lean
+++ b/tests/lean/tst5.lean
@@ -1,3 +1,4 @@
+universe U >= 3
 variable N : Type
 variable a : N
 variable b : N
diff --git a/tests/lean/type_inf_bug1.lean b/tests/lean/type_inf_bug1.lean
index eb1f1e326..75458f944 100644
--- a/tests/lean/type_inf_bug1.lean
+++ b/tests/lean/type_inf_bug1.lean
@@ -1,5 +1,8 @@
 import cast
 set::option pp::colors false
+universe M >= 1
+universe U >= M + 1
+definition TypeM := (Type M)
 
 check fun (A A': TypeM)
           (a   : A)
diff --git a/tests/lean/type_inf_bug1.lean.expected.out b/tests/lean/type_inf_bug1.lean.expected.out
index 9da17743b..0e2af54dc 100644
--- a/tests/lean/type_inf_bug1.lean.expected.out
+++ b/tests/lean/type_inf_bug1.lean.expected.out
@@ -2,6 +2,7 @@
   Set: pp::unicode
   Imported 'cast'
   Set: pp::colors
+  Defined: TypeM
 λ (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), let b' : A := cast L2 b, L3 : b == b' := cast::eq L2 b in L3 :
     ∀ (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), b == cast L2 b
 λ (A A' : TypeM)
diff --git a/tests/lean/univ.lean b/tests/lean/univ.lean
index 504c4effd..16397efc9 100644
--- a/tests/lean/univ.lean
+++ b/tests/lean/univ.lean
@@ -1,4 +1,7 @@
 
+universe M >= 1
+universe U >= M + 1
+definition TypeM := (Type M)
 universe Z ≥ M+3
 (*
 local env = get_environment()
diff --git a/tests/lean/univ.lean.expected.out b/tests/lean/univ.lean.expected.out
index e326845ac..2b668484b 100644
--- a/tests/lean/univ.lean.expected.out
+++ b/tests/lean/univ.lean.expected.out
@@ -1,4 +1,5 @@
   Set: pp::colors
   Set: pp::unicode
-Error (line: 27, pos: 0) universe constraint produces an integer overflow: Z2 >= Z1 + 1073741824
-Error (line: 40, pos: 0) universe constraint inconsistency: U1 >= U4 + 0
+  Defined: TypeM
+Error (line: 30, pos: 0) universe constraint produces an integer overflow: Z2 >= Z1 + 1073741824
+Error (line: 43, pos: 0) universe constraint inconsistency: U1 >= U4 + 0
diff --git a/tests/lean/univ2.lean b/tests/lean/univ2.lean
index 00ea05ce6..1a67e40f8 100644
--- a/tests/lean/univ2.lean
+++ b/tests/lean/univ2.lean
@@ -1,7 +1,9 @@
+universe M >= 1
+universe U >= M + 1
 universe Z >= max U+1 M+1
 print environment 2
 (*
 local env = get_environment()
 assert(env:get_universe_distance("Z", "U") == 1)
-assert(env:get_universe_distance("Z", "M") == 513)
+assert(env:get_universe_distance("Z", "M") == 2)
 *)
diff --git a/tests/lean/univ2.lean.expected.out b/tests/lean/univ2.lean.expected.out
index d7a2c5f98..d62395bb1 100644
--- a/tests/lean/univ2.lean.expected.out
+++ b/tests/lean/univ2.lean.expected.out
@@ -1,5 +1,4 @@
   Set: pp::colors
   Set: pp::unicode
-import "kernel"
-import "Nat"
+universe U ≥ M+1
 universe Z ≥ U+1 ⊔ M+1