mbenke / hm-typecheck

Experimental typechecker for a Solidity intermediate language
3 stars 1 forks source link

Fix core generation for functions not in eta-long form #3

Closed mbenke closed 2 months ago

mbenke commented 3 months ago

$ cabal run fun examples/mona/02id3.fun examples/mona/02id3.fun id x = x; nid = id; main = id (nid 42)

id : ∀a.a -> a main : Int nid : ∀a.a -> a


Resolutions:

id : b -> b = (x:b) -> (x: b) main : Int = (id: Int -> Int) ((nid: Int -> Int) 42) nid : d -> d = (id: d -> d)


Specialised:

id$Int = (x:Int) -> (x: Int) main = (id$Int: Int -> Int) ((nid$Int: Int -> Int) 42) nid$Int = (id$Int: Int -> Int)


Core:

function id$Int (x : int) -> int { return x fun: Cannot translate function type Int -> Int CallStack (from HasCallStack): error, called at src/Language/Fun/EmitCore.hs:182:31 in hm-0.1.0.0-inplace:Language.Fun.EmitCore translateType, called at src/Language/Fun/EmitCore.hs:53:20 in hm-0.1.0.0-inplace:Language.Fun.EmitCore

mbenke commented 3 months ago

id is in eta-long form and translates correctly. OTOH nid is not eta-long and fails to translate.

mbenke commented 2 months ago

Solved by 9e4e1c6