search

edwinb / Idris2-boot

A dependently typed programming language, a successor to Idris
https://idris-lang.org/
Other
902 stars 57 forks source link

Module import unstable #129

Open ohad opened 5 years ago

ohad commented 5 years ago

I'm not sure this is a bug, it's possible my types are not quite right, or that I've used access modifiers the wrong way.

Steps to Reproduce

Download the attached unstable-import.zip and unpack, and build it.

$ unzip unstable-import.zip
Archive:  unstable-import.zip
  inflating: PreorderReasoning.idr  
  inflating: VectReasoning.idr  
  inflating: Carriers.idr      
  inflating: Signatures.idr    
  inflating: Algebras.idr      
  inflating: Presentations.idr  
  inflating: Models.idr        
  inflating: Frex.idr          
  inflating: Monoids.idr       
  inflating: Powers.idr        
  inflating: CMonoids.idr      
  inflating: CMonoids/Axioms.idr  
  inflating: CMonoids/Nat.idr  
  inflating: CMonoids/Semiring.idr  
  inflating: CMonoids/Free.idr 
$ idris2 -c CMonoids.idr

Expected Behavior

Build should complete successfully:

$ idris2 -c CMonoids.idr 
1/15: Building PreorderReasoning (PreorderReasoning.idr)
2/15: Building VectReasoning (VectReasoning.idr)
3/15: Building Carriers (Carriers.idr)
4/15: Building Signatures (Signatures.idr)
5/15: Building Algebras (Algebras.idr)
6/15: Building Presentations (Presentations.idr)
7/15: Building Models (Models.idr)
8/15: Building Frex (Frex.idr)
9/15: Building Monoids (Monoids.idr)
10/15: Building CMonoids.Axioms (CMonoids/Axioms.idr)
11/15: Building CMonoids.Nat (CMonoids/Nat.idr)
12/15: Building Powers (Powers.idr)
13/15: Building CMonoids.Semiring (CMonoids/Semiring.idr)
14/15: Building CMonoids.Free (CMonoids/Free.idr)
15/15: Building CMonoids (CMonoids.idr)
$

Observed Behavior

...
15/15: Building CMonoids (CMonoids.idr)
CMonoids.idr:31:39--32:1:While processing type of CMonoids.CMonoid_free_up_uniqueness at CMonoids.idr:23:1--32:1:
When unifying U (Alg b) and U (Alg b)
Mismatch between:
    S (S Z)
and
    Z

so far so good, but if you edit CMonoids.idr and change line 16 onward as follows, moving the import of CMonoids.Semiring two imports down:

--import CMonoids.Semiring

import public CMonoids.Axioms
import public CMonoids.Nat
import        CMonoids.Semiring
import public CMonoids.Free

then everything type-checks fine:

$ idris2 -c CMonoids.idr 
15/15: Building CMonoids (CMonoids.idr)
$

This can also be expected if somehow these modules exported an ambiguity in definitions, but I think they don't.

ohad commented 5 years ago

Oh yes, you'll need to increase the stack size by building with the appropriate flag on Windows (see #117 ) or something like ulimit -s 16000 on Linux.

edwinb commented 4 years ago

I haven't checked if it affects this issue, but recently I found and fixed a problem with 'import public', so maybe this is okay now?

ohad commented 4 years ago 
$ idris2 --version
Idris 2, version 0.0.0-22a779bc8
$ idris2 -c CMonoids.idr 
1/15: Building PreorderReasoning (PreorderReasoning.idr)
2/15: Building VectReasoning (VectReasoning.idr)
3/15: Building Carriers (Carriers.idr)
4/15: Building Signatures (Signatures.idr)
5/15: Building Algebras (Algebras.idr)
6/15: Building Presentations (Presentations.idr)
7/15: Building Models (Models.idr)
8/15: Building Frex (Frex.idr)
9/15: Building Monoids (Monoids.idr)
10/15: Building CMonoids.Axioms (CMonoids/Axioms.idr)
11/15: Building CMonoids.Nat (CMonoids/Nat.idr)
12/15: Building Powers (Powers.idr)
13/15: Building CMonoids.Semiring (CMonoids/Semiring.idr)
14/15: Building CMonoids.Free (CMonoids/Free.idr)
15/15: Building CMonoids (CMonoids.idr)
CMonoids.idr:31:39--32:1:While processing type of CMonoids.CMonoid_free_up_uniqueness at CMonoids.idr:23:1--32:1:
When unifying U (Alg b) and U (Alg b)
Mismatch between:
    S (S Z)
and
    Z
ohad commented 4 years ago

And in case this is helpful (I added a newline, for readability)

CMonoids> :show_implicits
Parse error: Unrecognised command (next tokens: [identifier show_implicits, end of input])
CMonoids> :set showimplicits
CMonoids> :r
15/15: Building CMonoids (CMonoids.idr)
CMonoids.idr:31:39--32:1:While processing type of CMonoids.CMonoid_free_up_uniqueness at CMonoids.idr:23:1--32:1:
When unifying 
U {sig = MkDPair {a = Nat} {p = \n : Nat => Vect n Nat} (S (S Z)) (:: {len = S Z} {elem = Nat} Z (:: {len = Z} {elem = Nat} (S (S Z)) ([] {elem = Nat})))} (Alg {pres = PRESENTATION MONOID (S (S (S (S Z)))) (:: {len = S (S (S Z))} {elem = Equation (Sig Monoid_Th)} (Eq {sig = MkDPair {a = Nat} {p = \n : Nat => Vect n Nat} (S (S Z)) (:: {len = S Z} {elem = Nat} Z (:: {len = Z} {elem = Nat} (S (S Z)) ([] {elem = Nat})))} (S (S Z)) (Call {x = Fin (S (S Z))} {sig = MkDPair {a = Nat} {p = \n : Nat => Vect n Nat} (S (S Z)) (:: {len = S Z} {elem = Nat} Z (:: {len = Z} {elem = Nat} (S (S Z)) ([] {elem = Nat})))} .* (:: {len = S Z} {elem = Term (MkDPair {a = Nat} {p = \n : Nat => Vect n Nat} (S (S Z)) (:: {len = S Z} {elem = Nat} Z (:: {len = Z} {elem = Nat} (S (S Z)) ([] {elem = Nat})))) (Fin (S (S Z)))} (Done {sig = MkDPair {a = Nat} {p = \n : Nat => Vect n Nat} (S (S Z)) (:: {len = S Z} {elem = Nat} Z (:: {len = Z} {elem = Nat} (S (S Z)) ([] {elem = Nat})))} {x = Fin (S (S Z))} (FZ {k = S Z})) (:: {len = Z} {elem = Term (MkDPair {a = Nat} {p = \n : Nat => Vect n Nat} (S (S Z)) (:: {len = S Z} {elem = Nat} Z (:: {len = Z} {elem = Nat} (S (S Z)) ([] {elem = Nat})))) (Fin (S (S Z)))} (Done {sig = MkDPair {a = Nat} {p = \n : Nat => Vect n Nat} (S (S Z)) (:: {len = S Z} {elem = Nat} Z (:: {len = Z} {elem = Nat} (S (S Z)) ([] {elem = Nat})))} {x = Fin (S (S Z))} (FS {k = S Z} (FZ {k = Z}))) ([] {elem = Term (MkDPair {a = Nat} {p = \n : Nat => Vect n Nat} (S (S Z)) (:: {len = S Z} {elem = Nat} Z (:: {len = Z} {elem = Nat} (S (S Z)) ([] {elem = Nat})))) (Fin (S (S Z)))})))) (Call {x = Fin (S (S Z))} {sig = MkDPair {a = Nat} {p = \n : Nat => Vect n Nat} (S (S Z)) (:: {len = S Z} {elem = Nat} Z (:: {len = Z} {elem = Nat} (S (S Z)) ([] {elem = Nat})))} .* (:: {len = S Z} {elem = Term (MkDPair {a = Nat} {p = \n : Nat => Vect n Nat} (S (S Z)) (:: {len = S Z} {elem = Nat} Z (:: {len = Z} {elem = Nat} (S (S Z)) ([] {elem = Nat})))) (Fin (S (S Z)))} (Done {sig = MkDPair {a = Nat} {p = \n : Nat => Vect n Nat} (S (S Z)) (:: {len = S Z} {elem = Nat} Z (:: {len = Z} {elem = Nat} (S (S Z)) ([] {elem = Nat})))} {x = Fin (S (S Z))} (FS {k = S Z} (FZ {k = Z}))) (:: {len = Z} {elem = Term (MkDPair {a = Nat} {p = \n : Nat => Vect n Nat} (S (S Z)) (:: {len = S Z} {elem = Nat} Z (:: {len = Z} {elem = Nat} (S (S Z)) ([] {elem = Nat})))) (Fin (S (S (S (S Z)))))} (Done {sig = MkDPair {a = Nat} {p = \n : Nat => Vect n Nat} (S (S Z)) (:: {len = S Z} {elem = Nat} Z (:: {len = Z} {elem = Nat} (S (S Z)) ([] {elem = Nat})))} {x = Fin (S (S (S (S Z))))} (FZ {k = S (S (S Z))})) ([] {elem = Term (MkDPair {a = Nat} {p = \n : Nat => Vect n Nat} (S (S Z)) (:: {len = S Z} {elem = Nat} Z (:: {len = Z} {elem = Nat} (S (S Z)) ([] {elem = Nat})))) (Fin (S (S (S (S Z)))))}))))) (Ax Monoid_Th))} b) 
and 
U {sig = MkDPair {a = Nat} {p = \n : Nat => Vect n Nat} (S (S Z)) (:: {len = S Z} {elem = Nat} Z (:: {len = Z} {elem = Nat} (S (S Z)) ([] {elem = Nat})))} (Alg {pres = PRESENTATION MONOID (S (S (S (S Z)))) (:: {len = S (S (S Z))} {elem = Equation (Sig Monoid_Th)} (Eq {sig = MkDPair {a = Nat} {p = \n : Nat => Vect n Nat} (S (S Z)) (:: {len = S Z} {elem = Nat} Z (:: {len = Z} {elem = Nat} (S (S Z)) ([] {elem = Nat})))} (S (S Z)) (Call {x = Fin (S (S Z))} {sig = MkDPair {a = Nat} {p = \n : Nat => Vect n Nat} (S (S Z)) (:: {len = S Z} {elem = Nat} Z (:: {len = Z} {elem = Nat} (S (S Z)) ([] {elem = Nat})))} .* (:: {len = S Z} {elem = Term (MkDPair {a = Nat} {p = \n : Nat => Vect n Nat} (S (S Z)) (:: {len = S Z} {elem = Nat} Z (:: {len = Z} {elem = Nat} (S (S Z)) ([] {elem = Nat})))) (Fin (S (S Z)))} (Done {sig = MkDPair {a = Nat} {p = \n : Nat => Vect n Nat} (S (S Z)) (:: {len = S Z} {elem = Nat} Z (:: {len = Z} {elem = Nat} (S (S Z)) ([] {elem = Nat})))} {x = Fin (S (S Z))} (FZ {k = S Z})) (:: {len = Z} {elem = Term (MkDPair {a = Nat} {p = \n : Nat => Vect n Nat} (S (S Z)) (:: {len = S Z} {elem = Nat} Z (:: {len = Z} {elem = Nat} (S (S Z)) ([] {elem = Nat})))) (Fin (S (S Z)))} (Done {sig = MkDPair {a = Nat} {p = \n : Nat => Vect n Nat} (S (S Z)) (:: {len = S Z} {elem = Nat} Z (:: {len = Z} {elem = Nat} (S (S Z)) ([] {elem = Nat})))} {x = Fin (S (S Z))} (FS {k = S Z} (FZ {k = Z}))) ([] {elem = Term (MkDPair {a = Nat} {p = \n : Nat => Vect n Nat} (S (S Z)) (:: {len = S Z} {elem = Nat} Z (:: {len = Z} {elem = Nat} (S (S Z)) ([] {elem = Nat})))) (Fin (S (S Z)))})))) (Call {x = Fin (S (S Z))} {sig = MkDPair {a = Nat} {p = \n : Nat => Vect n Nat} (S (S Z)) (:: {len = S Z} {elem = Nat} Z (:: {len = Z} {elem = Nat} (S (S Z)) ([] {elem = Nat})))} .* (:: {len = S Z} {elem = Term (MkDPair {a = Nat} {p = \n : Nat => Vect n Nat} (S (S Z)) (:: {len = S Z} {elem = Nat} Z (:: {len = Z} {elem = Nat} (S (S Z)) ([] {elem = Nat})))) (Fin (S (S Z)))} (Done {sig = MkDPair {a = Nat} {p = \n : Nat => Vect n Nat} (S (S Z)) (:: {len = S Z} {elem = Nat} Z (:: {len = Z} {elem = Nat} (S (S Z)) ([] {elem = Nat})))} {x = Fin (S (S Z))} (FS {k = S Z} (FZ {k = Z}))) (:: {len = Z} {elem = Term (MkDPair {a = Nat} {p = \n : Nat => Vect n Nat} (S (S Z)) (:: {len = S Z} {elem = Nat} Z (:: {len = Z} {elem = Nat} (S (S Z)) ([] {elem = Nat})))) (Fin (S (S Z)))} (Done {sig = MkDPair {a = Nat} {p = \n : Nat => Vect n Nat} (S (S Z)) (:: {len = S Z} {elem = Nat} Z (:: {len = Z} {elem = Nat} (S (S Z)) ([] {elem = Nat})))} {x = Fin (S (S Z))} (FZ {k = S Z})) ([] {elem = Term (MkDPair {a = Nat} {p = \n : Nat => Vect n Nat} (S (S Z)) (:: {len = S Z} {elem = Nat} Z (:: {len = Z} {elem = Nat} (S (S Z)) ([] {elem = Nat})))) (Fin (S (S Z)))}))))) (Ax Monoid_Th))} b)
Mismatch between:
    S (S Z)
and
    Z

Also, commenting out the import CMonoids.Semiring compiles fine, as in the report above.

ohad commented 4 years ago

(You can see where the two lines start to differ --- I'm not sure whether that's a problem or not, but the import shouldn't affect this, I think.