Skip to content

Commit

Permalink
Don't generalize a rec. group, if any members are marked as monomorphic.
Browse files Browse the repository at this point in the history
Fixes #607
  • Loading branch information
yav committed Jun 14, 2019
1 parent 155e5ea commit ec7c9a0
Show file tree
Hide file tree
Showing 3 changed files with 15 additions and 5 deletions.
12 changes: 7 additions & 5 deletions src/Cryptol/TypeCheck/Infer.hs
Original file line number Diff line number Diff line change
Expand Up @@ -642,7 +642,10 @@ inferCArm armNum (m : ms) =
return (m1 : ms', Map.insertWith (\_ old -> old) x t ds, tMul n n')

-- | @inferBinds isTopLevel isRec binds@ performs inference for a
-- strongly-connected component of 'P.Bind's. If @isTopLevel@ is true,
-- strongly-connected component of 'P.Bind's.
-- If any of the members of the recursive group are already marked
-- as monomorphic, then we don't do generalzation.
-- If @isTopLevel@ is true,
-- any bindings without type signatures will be generalized. If it is
-- false, and the mono-binds flag is enabled, no bindings without type
-- signatures will be generalized, but bindings with signatures will
Expand All @@ -653,12 +656,11 @@ inferBinds isTopLevel isRec binds =
-- declarations, mark all bindings lacking signatures as monomorphic
monoBinds <- getMonoBinds
let (sigs,noSigs) = partition (isJust . P.bSignature) binds
monos = [ b { P.bMono = True } | b <- noSigs ]
binds' | monoBinds && not isTopLevel = sigs ++ monos
monos = sigs ++ [ b { P.bMono = True } | b <- noSigs ]
binds' | any P.bMono binds = monos
| monoBinds && not isTopLevel = monos
| otherwise = binds



check exprMap =
{- Guess type is here, because while we check user supplied signatures
we may generate additional constraints. For example, `x - y` would
Expand Down
3 changes: 3 additions & 0 deletions tests/issues/issue607.icry
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
let (x,y)=(0,x+1)
x
y
5 changes: 5 additions & 0 deletions tests/issues/issue607.icry.stdout
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
Loading module Cryptol
[warning] at <interactive>:1:5--1:18:
Defaulting the type of '<interactive>::y' to [1]
0x0
0x1

0 comments on commit ec7c9a0

Please sign in to comment.