This commit is contained in:
Paul Chiusano 2023-07-20 22:57:04 -04:00
parent 66dc3b0c3d
commit e25d0965bb
3 changed files with 4 additions and 4 deletions

View File

@ -1249,7 +1249,7 @@ synthesizeWanted e
et = existential' l B.Blank e
appendContext $
[existential i, existential e, existential o, Ann arg it]
when (Var.typeOf i == Var.Delay) $ do
when (Var.typeOf i == Var.Delay) $ do
-- '(1 + 1) turns into a lambda with an arg variable of type Var.Delay
-- here's where the typechecker assumes this must be of type 'thunkArgType'
subtype it (DDB.thunkArgType l)

View File

@ -630,8 +630,8 @@ pattern Delay' body <- (unDelay -> Just body)
unDelay :: (Var v) => Term2 vt at ap v a -> Maybe (Term2 vt at ap v a)
unDelay tm = case ABT.out tm of
ABT.Tm (Lam (ABT.Term _ _ (ABT.Abs v body)))
| Var.typeOf v == Var.Delay || Var.typeOf v == Var.User "()"
-> Just body
| Var.typeOf v == Var.Delay || Var.typeOf v == Var.User "()" ->
Just body
_ -> Nothing
pattern LamNamed' ::

View File

@ -175,7 +175,7 @@ data Type
| -- A variable for situations where we need to make up one that
-- definitely won't be used.
Irrelevant
| -- A variable used to represent the ignored argument to a thunk, as in '(1 + 1)
| -- A variable used to represent the ignored argument to a thunk, as in '(1 + 1)
Delay
deriving (Eq, Ord, Show)