search

svenssonjoel / Sense-VM

Sense-VM has changed name to SynchronVM and is available in a new repository https://github.com/SynchronVM/SynchronVM
MIT License
5 stars 1 forks source link

Desugaring/Typechecking bug #8

Open Abhiroop opened 3 years ago

Abhiroop commented 3 years ago

This program fails:

data List a where
  Nil  : List a
  Cons : a -> List a -> List a

baz = let (Cons x _) = (Cons 1 Nil)
       in (x + x)

Fails with

let v7 = \ v5 -> \ v6 -> (Cons2 (v5, v6)) in let v8 = (Nil3) in let v0 = let (Cons2 (v1, _)*** Exception: Maybe.fromJust: Nothing
CallStack (from HasCallStack):
  error, called at libraries/base/Data/Maybe.hs:148:21 in base:Data.Maybe
  fromJust, called at /Users/abhiroopsarkar/C/Sense-VM/frontend/CamIoT/src/Desugaring/Desugar.hs:30:53 in main:Desugaring.Desugar
Abhiroop commented 3 years ago 
data List a where {
  Nil : List a;
  Cons : a -> List a -> List a
}
v0 = let (Cons v1 _) = Cons 1 Nil in v1 + v1 :  Int

main = v0 :  n

The issue seems to be in the monomorphiser which is unable to monomorphise the main function. Notice the polymorphic type of the main.

It eventually eliminates the main function assuming there is no call to main and hence it is safe to remove.

Rewbert commented 3 years ago

The issue is probably in the type checker, where it doesn't unify the type of main and baz properly.

Rewbert commented 3 years ago

Smaller test case the replicate the same bug:

baz = let x = 1
      in x

main = baz

The issue is probably that the type of the entire let expression is placed in the environment after the let expression has returned (and thus returned the typing environment to the same state), so the type of baz will become the type schema forall b . b, where it should be forall () . b. When main looks up the type of baz, b will be instantiated to a fresh type variable.