fix more tyapps

ElaraLang · Dec 15, 2023 · 70aae06 · 70aae06
1 parent da17b7c
commit 70aae06
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 6 deletions.
diff --git a/src/Elara/AST/Generic/Instances/Pretty.hs b/src/Elara/AST/Generic/Instances/Pretty.hs
@@ -105,7 +105,7 @@ instance
     Pretty (Expr ast)
     where
     pretty =
-        let ?withType = True
+        let ?withType = False
             ?contextFree = True
          in prettyExpr @ast @exprType @letPatterns @lambdaPatterns
 

diff --git a/src/Elara/TypeInfer/Infer.hs b/src/Elara/TypeInfer/Infer.hs
@@ -23,7 +23,7 @@
 -}
 module Elara.TypeInfer.Infer where
 
-import Control.Lens ((^.), _1, _2)
+import Control.Lens (view, (^.), _1, _2)
 import Data.Generics.Wrapped
 import Data.List.NonEmpty qualified as NE
 import Data.Map qualified as Map
@@ -1369,7 +1369,7 @@ infer (Syntax.Expr (Located location e0, _)) = case e0 of
 
         ctx <- get
         completedFunctionType <- Context.complete ctx (Type.stripForAll (Syntax.typeOf _A)) -- I don't like that this is necessary but we get redundant type applications otherwise
-        let isFreeTypeVariable = \case Type.VariableType _ x -> not (Type.occurs x completedFunctionType); Type.UnsolvedType{} -> True; _ -> False
+        let isFreeTypeVariable = \case Type.VariableType _ x -> x `elem` (view unlocated <$> Type.freeTypeVars completedFunctionType); Type.UnsolvedType{} -> True; _ -> False
         let argLoc = typedArgument ^. exprLocation
         let resultLoc = resultType.location
         e <- case Type.stripForAll completedFunctionType of
@@ -1405,10 +1405,11 @@ infer (Syntax.Expr (Located location e0, _)) = case e0 of
                             typedArgument
             Type.Function{output}
                 | isFreeTypeVariable output -> do
-                    debugPretty ("out" :: Text, Type.stripForAll resultType)
+                    _0 <- get
+                    let solved = Context.solveType _0 resultType
                     pure $
                         FunctionCall
-                            ( Expr (Located resultLoc (TypeApplication _A (Type.stripForAll resultType)), resultType)
+                            ( Expr (Located resultLoc (TypeApplication _A (Type.applicableTyApp completedFunctionType resultType)), resultType)
                             )
                             typedArgument
             _ -> do
@@ -1623,7 +1624,7 @@ check expr@(Expr (Located exprLoc _, _)) t = do
 
         subtype (Context.solveType _Θ _At) (Context.solveType _Θ _B)
         case _At of
-            Type.Forall{} | Type.isMonoType t -> do
+            Type.Forall{} | _At `Type.instantiate` t /= _At -> do
                 -- insert type application from instantiating the forall
                 debugPretty ("instantiate" :: Text, _At, t, _At `Type.instantiate` t)
                 debugPretty (Context.solveType _Θ _At, Context.solveType _Θ _B)

diff --git a/src/Elara/TypeInfer/Type.hs b/src/Elara/TypeInfer/Type.hs
@@ -228,6 +228,7 @@ to determine the type of the type application, as naively we would instantiate i
 which is actually incorrect.
 -}
 applicableTyApp :: Show s => Type s -> Type s -> Type s
+applicableTyApp _ y@(UnsolvedType{}) = y
 applicableTyApp (Forall{name, type_ = VariableType{name = n}}) y | name == n = y
 applicableTyApp (Forall{name, type_ = Function{input = VariableType{name = n}}}) Function{input = sIn}
     | name == n = sIn