Skip to content

Instantly share code, notes, and snippets.

@jbrown215
Last active Oct 27, 2017
Embed
What would you like to do?
LiquidHaskell Copyright 2013-17 Regents of the University of California. All Rights Reserved.
**** DONE: A-Normalization ****************************************************
**** DONE: Extracted Core using GHC *******************************************
**** DONE: Transformed Core ***************************************************
**** DONE: Uniqify & Rename ***************************************************
Working 100% [=================================================================]
**** DONE: annotate ***********************************************************
**** RESULT: UNSAFE ************************************************************
/Users/JordanBrown/research/binah/db/world/World.hs:22:1-8: Error: Liquid Type Mismatch
22 | makeBlob () = Blob {xVal = 3, yVal = 4}
^^^^^^^^
Inferred type
VV : {v : Blob | World.yVal v == ?b
&& World.xVal v == ?a}
not a subtype of Required type
VV : {VV : Blob | World.xVal VV == World.xVal canonicalBlob}
In Context
?b : {?b : Int | ?b == (4 : int)}
?a : {?a : Int | ?a == (3 : int)}
/Users/JordanBrown/research/binah/db/world/World.hs:25:1-9: Error: Liquid Type Mismatch
25 | makeRange () = Range {lower = 3, upper = 4}
^^^^^^^^^
Inferred type
VV : {v : Int | v == (3 : int)
&& v == ?a}
not a subtype of Required type
VV : {VV : Int | VV == World.xVal canonicalBlob}
In Context
?a : {?a : Int | ?a == (3 : int)}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment