first record forallness fix?

src/Compiler/TypeInference.elm

@@ -25,7 +25,7 @@ type alias Name =
 
 type alias Env =
     { instanceVariables : Dict Name InstanceVariable
-    , typeVariables : Dict Name TypeVariable
+    , constrainedTypeVariables : Dict Name TypeVariable
 
     -- TODO env should also collect information about the context, to be used in error messages?
     }
@@ -34,7 +34,7 @@ type alias Env =
 initEnv : Env
 initEnv =
     { instanceVariables = Dict.empty
-    , typeVariables = Dict.empty
+    , constrainedTypeVariables = Dict.empty
     }
 
 
@@ -338,17 +338,7 @@ fromDefinition env isMutable pattern maybeAnnotation body =
             --
             do (fromBlock env body) <| \bodyType ->
             do (fromPattern env pattern Dict.empty) <| \patternOut ->
-            let
-                _ = Debug.log "unify" (bodyType, patternOut.ty)
-            in
             do (unify patternOut.pos UnifyReason_DefBlockVsPattern bodyType patternOut.ty) <| \unifiedType ->
-            -- XXXXXXXXX apply subs should know that 0 is constrained?
-            {-
-                tyvar 0 is constrained
-                however, when it is replaced by 1, 1 is not constrained
-
-                Should applySubsToPatternVarsAndAddThemToEnv also apply subs to env.typeVariables?
-            -}
             do (applySubsToPatternVarsAndAddThemToEnv isMutable patternOut.vars env) <| return
 
         Just annotatedType ->
@@ -1016,19 +1006,13 @@ insertPatternVar subs isParameter isMutable name ( pos, ty ) env =
                     Set.empty
 
                 else
-                    let
-                        _ = Debug.log name (env.typeVariables, refinedTy, subs)
-                    in
-                    getFreeTypeVars env.typeVariables refinedTy
+                    getFreeTypeVars env.constrainedTypeVariables refinedTy
             }
             env.instanceVariables
-    , typeVariables =
+    , constrainedTypeVariables =
         if isParameter then
-            let
-                _ =
-                    Debug.log "---" (typeVarsFromType refinedTy)
-            in
             {-
+
                Within the function body, the type of the parameter must be considered non-free!
 
                Consider:
@@ -1040,17 +1024,41 @@ insertPatternVar subs isParameter isMutable name ( pos, ty ) env =
                if the type of `q` remains free, then every time we use `p`, `p` will get an entirely new type.
 
             -}
-            Set.foldl (\n -> Dict.insert n { definedAt = pos }) env.typeVariables (typeVarsFromType refinedTy)
+            Set.foldl (\n -> Dict.insert n { definedAt = pos }) env.constrainedTypeVariables (typeVarsFromType refinedTy)
 
         else
-            env.typeVariables
+            env.constrainedTypeVariables
     }
 
 
 applySubsToPatternVarsAndAddThemToEnv : Bool -> PatternVars -> Env -> Monad Env
 applySubsToPatternVarsAndAddThemToEnv isMutable vars env =
     do getSubstitutions <| \subs ->
-    return <| insertPatternVars subs False isMutable vars env
+    let
+        {-
+           Consider:
+
+           x q =
+                 { first } = q
+                 first
+
+           When we see that `q` must be a record, we need to replace its type.
+           However, because the type of `q` is a constrained type variable, we need to make sure that the type(s)
+           we use for the records are also constrained!
+
+        -}
+        meh typeVarName constrainedVars =
+            case Dict.get typeVarName subs of
+                Nothing ->
+                    constrainedVars
+
+                Just ty ->
+                    Set.foldl (\n -> Dict.insert n { definedAt = CA.posDummy }) constrainedVars (typeVarsFromType ty)
+
+        env1 =
+            { env | constrainedTypeVariables = List.foldl meh env.constrainedTypeVariables (Dict.keys env.constrainedTypeVariables) }
+    in
+    return <| insertPatternVars subs False isMutable vars env1
 
 
 replaceTypeVariablesWithNew : InstanceVariable -> Monad Type