Skip to content

Improve unification error when it fails #9

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
shulhi wants to merge 3 commits into
base: main
Choose a base branch
from
Open

Improve unification error when it fails #9

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
771a80b
Return unification error instead of empty list
shulhi Dec 23, 2022
5ee9202
Bump version
shulhi Dec 23, 2022
9dcd5f9
Merge branch 'main' into shulhi-improve-unification-error
shulhi Dec 23, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions inferno-core/CHANGELOG.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,7 @@
# Revision History for inferno-core

## 0.1.0.1 -- 2022-12-23
* Return unification error instead of empty list when unification failed

## 0.1.0.0 -- 2022-11-28
* Prepare for OSS release
2 changes: 1 addition & 1 deletion inferno-core/inferno-core.cabal
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
cabal-version: 2.4
name: inferno-core
version: 0.1.0.0
version: 0.1.0.1
synopsis: A statically-typed functional scripting language
description: Parser, type inference, and interpreter for a statically-typed functional scripting language
category: DSL,Scripting
Expand Down
26 changes: 16 additions & 10 deletions inferno-core/src/Inferno/Infer.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -43,7 +43,7 @@ import Data.Bifunctor (bimap)
import qualified Data.Bimap as Bimap
import Data.Either (partitionEithers, rights)
import Data.Generics.Product (HasType, getTyped, setTyped)
import Data.List (find, unzip4) -- intercalate
import qualified Data.List as List
import qualified Data.List.NonEmpty as NEList
import qualified Data.Map as Map
import qualified Data.Map.Merge.Lazy as Map
Expand Down Expand Up @@ -95,7 +95,7 @@ import Inferno.Types.Type
Substitutable (..),
TCScheme (..),
TV,
TypeClass (TypeClass),
TypeClass (..),
typeBool,
typeDouble,
typeInt,
Expand Down Expand Up @@ -381,7 +381,7 @@ inferTypeReps allTypeClasses (ForallTC tvs tyCls (ImplType _impl ty)) inputTys o
Left errs -> Left errs
Right subst ->
let tyClsSubst = Set.map (apply subst) tyCls
in case find (\(TypeClass nm _) -> nm == "rep") $ Set.toList tyClsSubst of
in case List.find (\(TypeClass nm _) -> nm == "rep") $ Set.toList tyClsSubst of

@goodlyrottenapple goodlyrottenapple Dec 27, 2022

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

hmm not sure why i wasn't just using set find here?? probably not terribly important tho

Nothing -> pure []
Just rep@(TypeClass _ runtimeRepTys) ->
if Set.null $ ftv rep
Expand Down Expand Up @@ -548,7 +548,7 @@ infer expr =
meta <- lookupEnv exprLoc (maybe (Right x) Left $ pinnedToMaybe mHash)
let (tcs, t@(ImplType impl t'')) = ty meta
attachTypeToPosition exprLoc meta
(expr', t') <- case find (\(TypeClass nm _) -> nm == "rep") $ Set.toList tcs of
(expr', t') <- case List.find (\(TypeClass nm _) -> nm == "rep") $ Set.toList tcs of
Just (TypeClass _ runtimeRepTys) -> do
implRepTyps <- forM runtimeRepTys $ \repTy -> do
i <- freshRaw
Expand Down Expand Up @@ -648,7 +648,7 @@ infer expr =
)
ArrayComp p1 e p2 sels cond p3 -> do
_ <- checkVariableOverlap $ NEList.toList sels
(sels', vars, is, css) <- unzip4 <$> go (NEList.toList sels) id
(sels', vars, is, css) <- List.unzip4 <$> go (NEList.toList sels) id

(e', ImplType i_e t_e, c_e) <- foldr inEnv (infer e) vars

Expand Down Expand Up @@ -704,7 +704,7 @@ infer expr =
checkVariableOverlap :: [(SourcePos, Ident, SourcePos, b, Maybe SourcePos)] -> Infer ()
checkVariableOverlap = \case
[] -> return ()
(loc, x, _, _e, _) : xs -> case find (\(_, x', _, _, _) -> x == x') xs of
(loc, x, _, _e, _) : xs -> case List.find (\(_, x', _, _, _) -> x == x') xs of
Just (loc', x', _, _, _) -> throwError [VarMultipleOccurrence x (elementPosition loc x) (elementPosition loc' x')]
Nothing -> checkVariableOverlap xs
Lam p1 args p2 e -> do
Expand Down Expand Up @@ -960,7 +960,7 @@ infer expr =
res <- forM (zip patVars $ map (\(_, _p, _, e'') -> e'') patExprs) $
\(vars, e''') -> foldr inEnv (infer e''') $ map (\(Ident x, meta) -> (ExtIdent $ Right x, meta)) vars

let (es'', is_res, ts_res, cs_res) = unzip4 $ map (\(e'', ImplType i_r t_r, cs_r) -> (e'', i_r, t_r, cs_r)) res
let (es'', is_res, ts_res, cs_res) = List.unzip4 $ map (\(e'', ImplType i_r t_r, cs_r) -> (e'', i_r, t_r, cs_r)) res
(isMerged, ics) = mergeImplicitMaps (blockPosition expr) (i_e : is_res)
tyCls = Set.fromList $ map snd $ rights $ Set.toList $ cs_e `Set.union` (Set.unions cs_res)
patTysEqConstraints =
Expand Down Expand Up @@ -1158,10 +1158,16 @@ unifies err (TSeries t1) (TSeries t2) = unifies err t1 t2
unifies err (TOptional t1) (TOptional t2) = unifies err t1 t2
unifies err (TTuple ts1) (TTuple ts2)
| length (tListToList ts1) == length (tListToList ts2) = unifyMany err (tListToList ts1) (tListToList ts2)
| List.null err =
let pos = initialPos ""
loc = (pos, pos)
in throwError [UnificationFail Set.empty (TTuple ts1) (TTuple ts2) loc]
| otherwise = throwError [UnificationFail (getTypeClassFromErrs err) (TTuple ts1) (TTuple ts2) loc | loc <- (getLocFromErrs err)]
Comment on lines +1161 to 1165

@goodlyrottenapple goodlyrottenapple Dec 27, 2022

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looking at this code, the error throwing doesn't really make sense. My original design is definitely wonky here. The idea behind throwing a list was to link several places in code which generate a contradiction. e.g. somewhere we assign a variable the value bool and elsewhere we try to add a number to it. the error should point to those two places in the code as a contradiction. However, I'm not sure this ever properly worked as intended. It seems we always just throw a singleton error anyway.

To get proper error location, we should probably track location for types we are unifying and then add those to the error when throwing, instead of adding a dummy pos. This will require a bit of a re-engineering tho.

unifies err _ _ =
-- trace "throwing in unifies " $
throwError err
unifies [] t1 t2 =
let pos = initialPos ""
loc = (pos, pos)
in throwError [UnificationFail Set.empty t1 t2 loc]
unifies err t1 t2 = throwError [UnificationFail (getTypeClassFromErrs err) t1 t2 loc | loc <- (getLocFromErrs err)]

-- Unification solver
solver :: Unifier -> Solve Subst
Expand Down